From 19ca95b1845dbf39941356e3958b5d6032618ea2 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 5 Oct 2023 19:52:52 +0000 Subject: [PATCH] chore: fix nonterminal simps (#7497) Fixes the nonterminal simps identified by #7496 --- Mathlib/Algebra/Hom/Centroid.lean | 2 +- Mathlib/Algebra/Homology/Single.lean | 2 +- Mathlib/Algebra/MonoidAlgebra/Basic.lean | 7 ++- Mathlib/Algebra/Order/Floor.lean | 2 +- Mathlib/Algebra/Order/LatticeGroup.lean | 2 +- Mathlib/Analysis/NormedSpace/AddTorsor.lean | 2 +- Mathlib/Analysis/NormedSpace/Banach.lean | 2 +- Mathlib/Analysis/NormedSpace/Multilinear.lean | 2 +- Mathlib/Analysis/SpecificLimits/Basic.lean | 2 +- Mathlib/CategoryTheory/Equivalence.lean | 2 +- Mathlib/CategoryTheory/Monoidal/Limits.lean | 8 ++- Mathlib/CategoryTheory/Monoidal/Mon_.lean | 4 +- Mathlib/Computability/Halting.lean | 5 +- Mathlib/Computability/Partrec.lean | 3 +- Mathlib/Computability/PartrecCode.lean | 4 +- Mathlib/Computability/Primrec.lean | 9 ++-- Mathlib/Computability/TMToPartrec.lean | 49 ++++++++++++------- Mathlib/Computability/TuringMachine.lean | 2 +- Mathlib/Data/Bitvec/Lemmas.lean | 2 +- Mathlib/Data/Fin/Basic.lean | 2 +- Mathlib/Data/Finset/Basic.lean | 4 +- Mathlib/Data/Finset/NoncommProd.lean | 2 +- Mathlib/Data/List/Chain.lean | 4 +- Mathlib/Data/List/NatAntidiagonal.lean | 4 +- Mathlib/Data/Multiset/Pi.lean | 2 +- Mathlib/Data/Multiset/Sections.lean | 2 +- Mathlib/Data/Nat/ModEq.lean | 2 +- Mathlib/Data/PEquiv.lean | 2 +- Mathlib/Data/PFunctor/Multivariate/M.lean | 2 +- Mathlib/Init/Data/Nat/Bitwise.lean | 5 +- Mathlib/LinearAlgebra/Orientation.lean | 2 +- .../LinearAlgebra/QuadraticForm/Basic.lean | 2 +- .../LinearAlgebra/TensorAlgebra/Basic.lean | 4 +- Mathlib/Logic/Encodable/Lattice.lean | 2 +- Mathlib/Logic/Equiv/Option.lean | 3 +- Mathlib/Logic/Equiv/TransferInstance.lean | 2 +- Mathlib/MeasureTheory/Measure/Hausdorff.lean | 2 +- .../MeasureTheory/Measure/OuterMeasure.lean | 11 +++-- Mathlib/ModelTheory/DirectLimit.lean | 4 +- Mathlib/NumberTheory/Dioph.lean | 6 +-- Mathlib/NumberTheory/Zsqrtd/Basic.lean | 2 +- Mathlib/SetTheory/Ordinal/Basic.lean | 2 +- Mathlib/SetTheory/Ordinal/Notation.lean | 3 +- Mathlib/Topology/Algebra/ValuedField.lean | 2 +- 44 files changed, 110 insertions(+), 79 deletions(-) diff --git a/Mathlib/Algebra/Hom/Centroid.lean b/Mathlib/Algebra/Hom/Centroid.lean index 7bbf2460bd193..f91a62f3b68f7 100644 --- a/Mathlib/Algebra/Hom/Centroid.lean +++ b/Mathlib/Algebra/Hom/Centroid.lean @@ -395,7 +395,7 @@ instance : Semiring (CentroidHom α) := toEnd_nat_cast theorem comp_mul_comm (T S : CentroidHom α) (a b : α) : (T ∘ S) (a * b) = (S ∘ T) (a * b) := by - simp + simp only [Function.comp_apply] rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left] #align centroid_hom.comp_mul_comm CentroidHom.comp_mul_comm diff --git a/Mathlib/Algebra/Homology/Single.lean b/Mathlib/Algebra/Homology/Single.lean index 69ace6a683167..4df4d18925d9e 100644 --- a/Mathlib/Algebra/Homology/Single.lean +++ b/Mathlib/Algebra/Homology/Single.lean @@ -437,7 +437,7 @@ def fromSingle₀Equiv (C : CochainComplex V ℕ) (X : V) : simp · exact hf · rw [C.shape, comp_zero] - simp + simp only [Nat.zero_eq, ComplexShape.up_Rel, zero_add] exact j.succ_succ_ne_one.symm } left_inv f := by ext i diff --git a/Mathlib/Algebra/MonoidAlgebra/Basic.lean b/Mathlib/Algebra/MonoidAlgebra/Basic.lean index 1b0b8a37fe10a..d2200f15769ff 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Basic.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Basic.lean @@ -600,7 +600,8 @@ theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_ -- Porting note: `reducible` cannot be `local` so the proof gets more complex. unfold MonoidAlgebra - simp + simp only [AddMonoidHom.coe_comp, Function.comp_apply, singleAddHom_apply, smulAddHom_apply, + smul_single, smul_eq_mul, AddMonoidHom.coe_mulLeft] rw [liftNC_single, liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc] #align monoid_algebra.lift_nc_smul MonoidAlgebra.liftNC_smul @@ -1117,7 +1118,9 @@ protected noncomputable def opRingEquiv [Monoid G] : refine AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₁ => AddMonoidHom.ext fun r₁ => AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₂ => AddMonoidHom.ext fun r₂ => ?_ -- Porting note: `reducible` cannot be `local` so proof gets long. - simp + simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, opAddEquiv_apply, + Function.comp_apply, singleAddHom_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.coe_mul, + AddMonoidHom.coe_mulLeft, AddMonoidHom.compl₂_apply] rw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, MulOpposite.opAddEquiv_symm_apply, MulOpposite.unop_mul (α := MonoidAlgebra k G)] diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean index 9a837c1994834..e48ac1e2b8988 100644 --- a/Mathlib/Algebra/Order/Floor.lean +++ b/Mathlib/Algebra/Order/Floor.lean @@ -304,7 +304,7 @@ theorem le_ceil (a : α) : a ≤ ⌈a⌉₊ := theorem ceil_intCast {α : Type*} [LinearOrderedRing α] [FloorSemiring α] (z : ℤ) : ⌈(z : α)⌉₊ = z.toNat := eq_of_forall_ge_iff fun a => by - simp + simp only [ceil_le, Int.toNat_le] norm_cast #align nat.ceil_int_cast Nat.ceil_intCast diff --git a/Mathlib/Algebra/Order/LatticeGroup.lean b/Mathlib/Algebra/Order/LatticeGroup.lean index 15f0c744322bb..2ca22ae839bd4 100644 --- a/Mathlib/Algebra/Order/LatticeGroup.lean +++ b/Mathlib/Algebra/Order/LatticeGroup.lean @@ -276,7 +276,7 @@ theorem mul_inf_eq_mul_inf_mul [CovariantClass α α (· * ·) (· ≤ ·)] (a b c * (a ⊓ b) = c * a ⊓ c * b := by refine' le_antisymm _ _ rw [le_inf_iff, mul_le_mul_iff_left, mul_le_mul_iff_left] - simp + simp only [inf_le_left, inf_le_right, and_self] rw [← mul_le_mul_iff_left c⁻¹, ← mul_assoc, inv_mul_self, one_mul, le_inf_iff, inv_mul_le_iff_le_mul, inv_mul_le_iff_le_mul] simp diff --git a/Mathlib/Analysis/NormedSpace/AddTorsor.lean b/Mathlib/Analysis/NormedSpace/AddTorsor.lean index db3a19c733c15..dea20580212af 100644 --- a/Mathlib/Analysis/NormedSpace/AddTorsor.lean +++ b/Mathlib/Analysis/NormedSpace/AddTorsor.lean @@ -298,7 +298,7 @@ def AffineMap.ofMapMidpoint (f : P → Q) (h : ∀ x y, f (midpoint ℝ x y) = m AffineMap.mk' f (↑((AddMonoidHom.ofMapMidpoint ℝ ℝ ((AffineEquiv.vaddConst ℝ (f <| c)).symm ∘ f ∘ AffineEquiv.vaddConst ℝ c) (by simp) fun x y => by -- Porting note: was `by simp [h]` - simp + simp only [Function.comp_apply, AffineEquiv.vaddConst_apply, AffineEquiv.vaddConst_symm_apply] conv_lhs => rw [(midpoint_self ℝ (Classical.arbitrary P)).symm, midpoint_vadd_midpoint, h, h, midpoint_vsub_midpoint]).toRealLinearMap <| by apply_rules [Continuous.vadd, Continuous.vsub, continuous_const, hfc.comp, continuous_id])) diff --git a/Mathlib/Analysis/NormedSpace/Banach.lean b/Mathlib/Analysis/NormedSpace/Banach.lean index 195d80bbf5995..b169c8fb78397 100644 --- a/Mathlib/Analysis/NormedSpace/Banach.lean +++ b/Mathlib/Analysis/NormedSpace/Banach.lean @@ -110,7 +110,7 @@ theorem exists_approx_preimage_norm_le (surj : Surjective f) : rw [← xz₁] at h₁ rw [mem_ball, dist_eq_norm, sub_zero] at hx₁ have : a ∈ ball a ε := by - simp + simp only [mem_ball, dist_self] exact εpos rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₂, z₂im, h₂⟩ rcases(mem_image _ _ _).1 z₂im with ⟨x₂, hx₂, xz₂⟩ diff --git a/Mathlib/Analysis/NormedSpace/Multilinear.lean b/Mathlib/Analysis/NormedSpace/Multilinear.lean index 9a56636cdc1c8..2de27620d4191 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear.lean @@ -215,7 +215,7 @@ theorem norm_image_sub_le_of_bound {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m · intro j _ by_cases h : j = i · rw [h] - simp + simp only [ite_true, Function.update_same] exact norm_le_pi_norm (m₁ - m₂) i · simp [h, -le_max_iff, -max_le_iff, max_le_max, norm_le_pi_norm (_ : ∀ i, E i)] _ = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 85225b916c181..9461b5bdca10a 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -269,7 +269,7 @@ theorem hasSum_geometric_two' (a : ℝ) : HasSum (fun n : ℕ => a / 2 / 2 ^ n) convert HasSum.mul_left (a / 2) (hasSum_geometric_of_lt_1 (le_of_lt one_half_pos) one_half_lt_one) using 1 · funext n - simp + simp only [one_div, inv_pow] rfl · norm_num #align has_sum_geometric_two' hasSum_geometric_two' diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean index eb634ea5c39ec..e37855e41ce92 100644 --- a/Mathlib/CategoryTheory/Equivalence.lean +++ b/Mathlib/CategoryTheory/Equivalence.lean @@ -258,7 +258,7 @@ def adjointifyη : 𝟭 C ≅ F ⋙ G := by theorem adjointify_η_ε (X : C) : F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) := by dsimp [adjointifyη,Trans.trans] - simp + simp only [comp_id, assoc, map_comp] have := ε.hom.naturality (F.map (η.inv.app X)); dsimp at this; rw [this]; clear this rw [← assoc _ _ (F.map _)] have := ε.hom.naturality (ε.inv.app <| F.obj X); dsimp at this; rw [this]; clear this diff --git a/Mathlib/CategoryTheory/Monoidal/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Limits.lean index 1aac3fbfaf3c9..7eb9628895f66 100644 --- a/Mathlib/CategoryTheory/Monoidal/Limits.lean +++ b/Mathlib/CategoryTheory/Monoidal/Limits.lean @@ -81,7 +81,9 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where dsimp; simp left_unitality X := by ext j; dsimp - simp + simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt, + Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj, + Monoidal.tensorUnit_obj, Monoidal.leftUnitor_hom_app] conv_rhs => rw [← tensor_id_comp_id_tensor (limit.π X j)] slice_rhs 1 2 => rw [← comp_tensor_id] @@ -91,7 +93,9 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where simp right_unitality X := by ext j; dsimp - simp + simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt, + Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj, + Monoidal.tensorUnit_obj, Monoidal.rightUnitor_hom_app] conv_rhs => rw [← id_tensor_comp_tensor_id _ (limit.π X j)] slice_rhs 1 2 => rw [← id_tensor_comp] diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean index b1e1e697de66b..d17ac70404739 100644 --- a/Mathlib/CategoryTheory/Monoidal/Mon_.lean +++ b/Mathlib/CategoryTheory/Monoidal/Mon_.lean @@ -380,7 +380,7 @@ variable {C} theorem one_associator {M N P : Mon_ C} : ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom = (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)) := by - simp + simp only [Category.assoc, Iso.cancel_iso_inv_left] slice_lhs 1 3 => rw [← Category.id_comp P.one, tensor_comp] slice_lhs 2 3 => rw [associator_naturality] slice_rhs 1 2 => rw [← Category.id_comp M.one, tensor_comp] @@ -449,7 +449,7 @@ theorem mul_associator {M N P : Mon_ C} : ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫ tensor_μ C (M.X, N.X ⊗ P.X) (M.X, N.X ⊗ P.X) ≫ (M.mul ⊗ tensor_μ C (N.X, P.X) (N.X, P.X) ≫ (N.mul ⊗ P.mul)) := by - simp + simp only [tensor_obj, prodMonoidal_tensorObj, Category.assoc] slice_lhs 2 3 => rw [← Category.id_comp P.mul, tensor_comp] slice_lhs 3 4 => rw [associator_naturality] slice_rhs 3 4 => rw [← Category.id_comp M.mul, tensor_comp] diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean index f08c76313733e..2a513d73756e4 100644 --- a/Mathlib/Computability/Halting.lean +++ b/Mathlib/Computability/Halting.lean @@ -180,7 +180,7 @@ protected theorem not {p : α → Prop} (hp : ComputablePred p) : ComputablePred exact ⟨by infer_instance, (cond hf (const false) (const true)).of_eq fun n => by - simp + simp only [Bool.not_eq_true] cases f n <;> rfl⟩ #align computable_pred.not ComputablePred.not @@ -253,7 +253,8 @@ theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] : cases hy.1 hx.1) · refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _ rw [hk] - simp + simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true, + Bool.true_eq_decide_iff, and_self, exists_const, Bool.false_eq_decide_iff] apply Decidable.em⟩⟩ #align computable_pred.computable_iff_re_compl_re ComputablePred.computable_iff_re_compl_re diff --git a/Mathlib/Computability/Partrec.lean b/Mathlib/Computability/Partrec.lean index e5b32a9fb28e5..45c19fd6448ba 100644 --- a/Mathlib/Computability/Partrec.lean +++ b/Mathlib/Computability/Partrec.lean @@ -224,7 +224,8 @@ theorem ppred : Partrec fun n => ppred n := eq_none_iff.2 fun a ⟨⟨m, h, _⟩, _⟩ => by simp [show 0 ≠ m.succ by intro h; injection h] at h · refine' eq_some_iff.2 _ - simp + simp only [mem_rfind, not_true, IsEmpty.forall_iff, decide_True, mem_some_iff, + Bool.false_eq_decide_iff, true_and] intro m h simp [ne_of_gt h] #align nat.partrec.ppred Nat.Partrec.ppred diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean index 95d5c55f26b17..9fe18359178ad 100644 --- a/Mathlib/Computability/PartrecCode.lean +++ b/Mathlib/Computability/PartrecCode.lean @@ -1125,7 +1125,7 @@ theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a rw [hg (Nat.pair_lt_pair_right _ lf)] cases n.unpair.2 · rfl - simp + simp only [decode_eq_ofNat, Option.some.injEq] rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)] cases evaln k' _ _ · rfl @@ -1134,7 +1134,7 @@ theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a rw [hg (Nat.pair_lt_pair_right _ lf)] cases' evaln k cf n with x · rfl - simp + simp only [decode_eq_ofNat, Option.some.injEq, Option.some_bind] cases x <;> simp [Nat.succ_ne_zero] rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)] (Primrec.option_bind diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean index ea35dc6263ced..55235365e9c98 100644 --- a/Mathlib/Computability/Primrec.lean +++ b/Mathlib/Computability/Primrec.lean @@ -343,7 +343,7 @@ theorem fst {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.fst α β (pair right ((@Primcodable.prim β).comp left)))).comp (pair right ((@Primcodable.prim α).comp left))).of_eq fun n => by - simp + simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val] cases @decode α _ n.unpair.1 <;> simp cases @decode β _ n.unpair.2 <;> simp #align primrec.fst Primrec.fst @@ -354,7 +354,7 @@ theorem snd {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.snd α β (pair right ((@Primcodable.prim β).comp left)))).comp (pair right ((@Primcodable.prim α).comp left))).of_eq fun n => by - simp + simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val] cases @decode α _ n.unpair.1 <;> simp cases @decode β _ n.unpair.2 <;> simp #align primrec.snd Primrec.snd @@ -568,7 +568,8 @@ theorem nat_rec {f : α → β} {g : α → ℕ × β → β} (hf : Primrec f) ( Nat.Primrec.right.pair <| Nat.Primrec.right.comp Nat.Primrec.left).comp <| Nat.Primrec.id.pair <| (@Primcodable.prim α).comp Nat.Primrec.left).of_eq fun n => by - simp + simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat, + Option.some_bind, Option.map_map, Option.map_some'] cases' @decode α _ n.unpair.1 with a; · rfl simp [encodek] induction' n.unpair.2 with m <;> simp [encodek] @@ -911,7 +912,7 @@ private theorem list_foldl' {f : α → List β} {g : α → σ} {h : α → σ generalize g a = x induction' n with n IH generalizing l x · rfl - simp + simp only [iterate_succ, comp_apply] cases' l with b l <;> simp [IH] private theorem list_cons' : (haveI := prim H; Primrec₂ (@List.cons β)) := diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 82bd137fd9656..3dbcf0bc71279 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -1356,7 +1356,7 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁ · rw [Function.update_noteq h₁.symm] rfl refine' TransGen.head' rfl _ - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq] revert e; cases' S k₁ with a Sk <;> intro e · cases e rfl @@ -1366,7 +1366,7 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁ · simp only [e] rfl · refine' TransGen.head rfl _ - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq, List.reverseAux_cons] cases' e₁ : S k₁ with a' Sk <;> rw [e₁, splitAtPred] at e · cases e cases e₂ : p a' <;> simp only [e₂, cond] at e @@ -1392,7 +1392,7 @@ theorem move₂_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k Reaches₁ (TM2.step tr) ⟨some (move₂ p k₁ k₂ q), s, S⟩ ⟨some q, none, update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂)⟩ := by refine' (move_ok h₁.1 e).trans (TransGen.head rfl _) - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, id_eq, ne_eq, Option.elim] cases o <;> simp only [Option.elim, id.def] · simp only [TM2.stepAux, Option.isSome, cond_false] convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2 @@ -1414,7 +1414,7 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p Reaches₁ (TM2.step tr) ⟨some (Λ'.clear p k q), s, S⟩ ⟨some q, o, update S k L₂⟩ := by induction' L₁ with a L₁ IH generalizing S s · refine' TransGen.head' rfl _ - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim] revert e; cases' S k with a Sk <;> intro e · cases e rfl @@ -1424,7 +1424,7 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p · rcases e with ⟨e₁, e₂⟩ rw [e₁, e₂] · refine' TransGen.head rfl _ - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim] cases' e₁ : S k with a' Sk <;> rw [e₁, splitAtPred] at e · cases e cases e₂ : p a' <;> simp only [e₂, cond] at e @@ -1444,7 +1444,9 @@ theorem copy_ok (q s a b c d) : · refine' TransGen.single _ simp refine' TransGen.head rfl _ - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some, + List.tail_cons, elim_update_rev, ne_eq, Function.update_noteq, elim_main, elim_update_main, + elim_stack, elim_update_stack, cond_true, List.reverseAux_cons] exact IH _ _ _ #align turing.partrec_to_TM2.copy_ok Turing.PartrecToTM2.copy_ok @@ -1483,7 +1485,8 @@ theorem head_main_ok {q s L} {c d : List Γ'} : (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) _)).trans (TransGen.head rfl (TransGen.head rfl _)) · cases L <;> simp - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_update_main, elim_rev, elim_update_rev, + Function.update_same, trList] rw [if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp)] refine' (clear_ok (splitAtPred_eq _ _ _ none [] _ ⟨rfl, rfl⟩)).trans _ · exact fun x h => Bool.decide_false (trList_ne_consₗ _ _ h) @@ -1500,7 +1503,9 @@ theorem head_stack_ok {q s L₁ L₂ L₃} : (move_ok (by decide) (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩)) (TransGen.head rfl (TransGen.head rfl _)) - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append, + elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_same, + List.headI_nil, trNat_default] convert unrev_ok using 2 simp · refine' @@ -1509,7 +1514,9 @@ theorem head_stack_ok {q s L₁ L₂ L₃} : (splitAtPred_eq _ _ (trNat a) (some Γ'.cons) (trList L₂ ++ Γ'.consₗ :: L₃) (trNat_natEnd _) ⟨rfl, by simp⟩)) (TransGen.head rfl (TransGen.head rfl _)) - simp + simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_false, trList, List.append_assoc, + List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_same, + List.headI_cons] refine' TransGen.trans (clear_ok @@ -1526,9 +1533,11 @@ theorem succ_ok {q s n} {c d : List Γ'} : simp [trNat, Num.add_one] cases' (n : Num) with a · refine' TransGen.head rfl _ - simp + simp only [Option.mem_def, TM2.stepAux, elim_main, decide_False, elim_update_main, ne_eq, + Function.update_noteq, elim_rev, elim_update_rev, decide_True, Function.update_same, + cond_true, cond_false] convert unrev_ok using 2 - simp + simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main] rfl simp [Num.succ, trNum, Num.succ'] suffices ∀ l₁, ∃ l₁' l₂' s', @@ -1548,7 +1557,8 @@ theorem succ_ok {q s n} {c d : List Γ'} : simp [PosNum.succ, trPosNum] rfl · refine' ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single _⟩ - simp + simp only [TM2.step, TM2.stepAux, elim_main, elim_update_main, ne_eq, Function.update_noteq, + elim_rev, elim_update_rev, Function.update_same, Option.mem_def, Option.some.injEq] rfl #align turing.partrec_to_TM2.succ_ok Turing.PartrecToTM2.succ_ok @@ -1567,7 +1577,9 @@ theorem pred_ok (q₁ q₂ s v) (c d : List Γ') : ∃ s', cases' (n : Num) with a · simp [trPosNum, trNum, show Num.zero.succ' = PosNum.one from rfl] refine' TransGen.head rfl _ - simp + simp only [Option.mem_def, TM2.stepAux, elim_main, List.head?_cons, Option.some.injEq, + decide_False, List.tail_cons, elim_update_main, ne_eq, Function.update_noteq, elim_rev, + elim_update_rev, natEnd, Function.update_same, cond_true, cond_false] convert unrev_ok using 2 simp simp [trNum, Num.succ'] @@ -1641,14 +1653,17 @@ theorem tr_ret_respects (k v s) : ∃ b₂, obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none refine' ⟨s', h₁, TransGen.head rfl _⟩; simp refine' (move₂_ok (by decide) _ (splitAtPred_false _)).trans _; · rfl - simp + simp only [TM2.step, Option.mem_def, Option.elim, id_eq, elim_update_main, elim_main, elim_aux, + List.append_nil, elim_update_aux] refine' (move₂_ok (by decide) _ _).trans _; pick_goal 4; · rfl pick_goal 4; · exact splitAtPred_eq _ _ _ (some Γ'.consₗ) _ (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, rfl⟩ refine' (move₂_ok (by decide) _ (splitAtPred_false _)).trans _; · rfl - simp + simp only [TM2.step, Option.mem_def, Option.elim, elim_update_stack, elim_main, + List.append_nil, elim_update_main, id_eq, elim_update_aux, ne_eq, Function.update_noteq, + elim_aux, elim_stack] exact h₂ case cons₂ ns k IH => obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none @@ -1734,13 +1749,13 @@ theorem trStmts₁_trans {q q'} : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trSt iterate 4 exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _) · simp intro s h x h' - simp + simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert] exact Or.inr ⟨_, q_ih s h h'⟩ · constructor · rintro rfl apply Finset.subset_insert · intro h x h' - simp + simp only [Finset.mem_insert] exact Or.inr (Or.inr <| q_ih h h') · refine' ⟨fun h x h' => _, fun _ x h' => _, fun h x h' => _⟩ <;> simp · exact Or.inr (Or.inr <| Or.inl <| q₁_ih h h') diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean index 39d7e83f37d6b..2fc68edd17f30 100644 --- a/Mathlib/Computability/TuringMachine.lean +++ b/Mathlib/Computability/TuringMachine.lean @@ -1840,7 +1840,7 @@ theorem stepAux_read (f : Γ → Stmt'₁) (v : σ) (L R : ListBlank Γ) : stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂)) · dsimp [readAux, stepAux] - simp + simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons] cases a <;> rfl rw [← ListBlank.append, IH] rfl diff --git a/Mathlib/Data/Bitvec/Lemmas.lean b/Mathlib/Data/Bitvec/Lemmas.lean index a5c9a4bea17d3..0c9ee560869e9 100644 --- a/Mathlib/Data/Bitvec/Lemmas.lean +++ b/Mathlib/Data/Bitvec/Lemmas.lean @@ -43,7 +43,7 @@ theorem toNat_append {m : ℕ} (xs : Bitvec m) (b : Bool) : conv in addLsb x b => rw [← h] clear h - simp + simp only [List.foldl_append, List.foldl_cons, List.foldl_nil] induction' xs with x xs xs_ih generalizing x · simp unfold addLsb diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 272d37cc63b15..24906d85cb343 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -1657,7 +1657,7 @@ theorem succAbove_predAbove {p : Fin n} {i : Fin (n + 1)} (h : i ≠ castSucc p) rw [if_pos] rfl exact H - simp + simp only [castSucc_mk, mk_lt_mk, not_lt] apply le_of_lt H · rw [dif_pos] rw [if_neg] diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index f2cc937d2da80..e0c32c2df34c9 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/Mathlib/Data/Finset/Basic.lean @@ -2802,7 +2802,7 @@ theorem subset_coe_filter_of_subset_forall (s : Finset α) {t : Set α} (h₁ : theorem filter_singleton (a : α) : filter p (singleton a) = if p a then singleton a else ∅ := by classical ext x - simp + simp only [mem_singleton, forall_eq, mem_filter] split_ifs with h <;> by_cases h' : x = a <;> simp [h, h'] #align finset.filter_singleton Finset.filter_singleton @@ -2930,7 +2930,7 @@ theorem subset_union_elim {s : Finset α} {t₁ t₂ : Set α} (h : ↑s ⊆ t · intro x simp · intro x - simp + simp only [not_not, coe_filter, Set.mem_setOf_eq, Set.mem_diff, and_imp] intro hx hx₂ refine' ⟨Or.resolve_left (h hx) hx₂, hx₂⟩ #align finset.subset_union_elim Finset.subset_union_elim diff --git a/Mathlib/Data/Finset/NoncommProd.lean b/Mathlib/Data/Finset/NoncommProd.lean index 5dda4fd402027..0500a70fabf84 100644 --- a/Mathlib/Data/Finset/NoncommProd.lean +++ b/Mathlib/Data/Finset/NoncommProd.lean @@ -427,7 +427,7 @@ theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) : · intro j _; dsimp · rw [noncommProd_insert_of_not_mem _ _ _ _ (not_mem_erase _ _), noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one] - simp + simp only [MonoidHom.single_apply, ne_eq, Pi.mulSingle_eq_same] · intro j hj simp at hj simp [Pi.mulSingle, Function.update] diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean index eaf52f6a9b080..a6378404a3ba4 100644 --- a/Mathlib/Data/List/Chain.lean +++ b/Mathlib/Data/List/Chain.lean @@ -352,7 +352,9 @@ theorem chain'_iff_get {R} : ∀ {l : List α}, Chain' R l ↔ | [a] => iff_of_true (by simp) (fun _ h => by simp at h) | a :: b :: t => by rw [← and_forall_succ, chain'_cons, chain'_iff_get] - simp + simp only [length_cons, get_cons_succ, Fin.zero_eta, get_cons_zero, zero_add, Fin.mk_one, + get_cons_cons_one, succ_sub_succ_eq_sub, nonpos_iff_eq_zero, add_eq_zero_iff, and_false, + tsub_zero, add_pos_iff, or_true, forall_true_left, and_congr_right_iff] dsimp [succ_sub_one] exact fun _ => ⟨fun h i hi => h i (Nat.lt_of_succ_lt_succ hi), fun h i hi => h i (Nat.succ_lt_succ hi)⟩ diff --git a/Mathlib/Data/List/NatAntidiagonal.lean b/Mathlib/Data/List/NatAntidiagonal.lean index 1e5d3bf896193..1c748478ebd45 100644 --- a/Mathlib/Data/List/NatAntidiagonal.lean +++ b/Mathlib/Data/List/NatAntidiagonal.lean @@ -86,7 +86,8 @@ theorem antidiagonal_succ_succ' {n : ℕ} : antidiagonal (n + 2) = (0, n + 2) :: (antidiagonal n).map (Prod.map Nat.succ Nat.succ) ++ [(n + 2, 0)] := by rw [antidiagonal_succ'] - simp + simp only [antidiagonal_succ, map_cons, Prod_map, id_eq, map_map, cons_append, cons.injEq, + append_cancel_right_eq, true_and] ext simp #align list.nat.antidiagonal_succ_succ' List.Nat.antidiagonal_succ_succ' @@ -102,4 +103,3 @@ theorem map_swap_antidiagonal {n : ℕ} : end Nat end List - diff --git a/Mathlib/Data/Multiset/Pi.lean b/Mathlib/Data/Multiset/Pi.lean index 865df3b312281..cc4fb517d717b 100644 --- a/Mathlib/Data/Multiset/Pi.lean +++ b/Mathlib/Data/Multiset/Pi.lean @@ -124,7 +124,7 @@ protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} : intro a s ih hs ht have has : a ∉ s := by simp at hs; exact hs.1 have hs : Nodup s := by simp at hs; exact hs.2 - simp + simp only [pi_cons, nodup_bind] refine' ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has), _⟩ diff --git a/Mathlib/Data/Multiset/Sections.lean b/Mathlib/Data/Multiset/Sections.lean index 37534ce84d29a..e4a363b1e3177 100644 --- a/Mathlib/Data/Multiset/Sections.lean +++ b/Mathlib/Data/Multiset/Sections.lean @@ -44,7 +44,7 @@ theorem coe_sections : (l.sections.map fun l : List α => (l : Multiset α) : Multiset (Multiset α)) | [] => rfl | a :: l => by - simp + simp only [List.map_cons, List.sections] rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l] simp [List.sections, (· ∘ ·), List.bind] #align multiset.coe_sections Multiset.coe_sections diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean index 74f0c46fae8cb..da8a9bbea7bd7 100644 --- a/Mathlib/Data/Nat/ModEq.lean +++ b/Mathlib/Data/Nat/ModEq.lean @@ -458,7 +458,7 @@ theorem add_div {a b c : ℕ} (hc0 : 0 < c) : by simpa only [mul_add, add_comm, add_left_comm, add_assoc] rw [mod_add_div, mod_add_div, mod_add_div, mul_ite, add_assoc, add_assoc] conv_lhs => rw [← add_mod_add_ite] - simp + simp only [mul_one, mul_zero] ac_rfl #align nat.add_div Nat.add_div diff --git a/Mathlib/Data/PEquiv.lean b/Mathlib/Data/PEquiv.lean index 0ae518f7f0da1..b2958bfe7fb52 100644 --- a/Mathlib/Data/PEquiv.lean +++ b/Mathlib/Data/PEquiv.lean @@ -392,7 +392,7 @@ theorem trans_single_of_eq_none {b : β} (c : γ) {f : δ ≃. β} (h : f.symm b ext simp only [eq_none_iff_forall_not_mem, Option.mem_def, f.eq_some_iff] at h dsimp [PEquiv.trans, single] - simp + simp only [mem_def, bind_eq_some, iff_false, not_exists, not_and] intros split_ifs <;> simp_all #align pequiv.trans_single_of_eq_none PEquiv.trans_single_of_eq_none diff --git a/Mathlib/Data/PFunctor/Multivariate/M.lean b/Mathlib/Data/PFunctor/Multivariate/M.lean index a90779275a58a..7caca4553e07f 100644 --- a/Mathlib/Data/PFunctor/Multivariate/M.lean +++ b/Mathlib/Data/PFunctor/Multivariate/M.lean @@ -335,7 +335,7 @@ theorem M.bisim₀ {α : TypeVec n} (R : P.M α → P.M α → Prop) (h₀ : Equ simpa using h₁ exists ax, dropFun fx, lastFun fx, lastFun fy rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun] - simp + simp only [true_and] intro i replace h₁ := congr_fun (congr_fun h₁ Fin2.fz) i simp [(· ⊚ ·), appendFun, splitFun] at h₁ diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean index 51a17ab3be68d..270ec0b011cfe 100644 --- a/Mathlib/Init/Data/Nat/Bitwise.lean +++ b/Mathlib/Init/Data/Nat/Bitwise.lean @@ -129,7 +129,7 @@ attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n | 0 => rfl | succ n => by - simp + simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm] refine' Eq.trans _ (congr_arg succ (bodd_add_div2 n)) cases bodd n <;> simp [cond, not] · rw [Nat.add_comm, Nat.add_succ] @@ -308,7 +308,8 @@ theorem binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (b theorem bodd_bit (b n) : bodd (bit b n) = b := by rw [bit_val] - simp + simp only [Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul, bodd_succ, bodd_zero, Bool.not_false, + Bool.not_true, Bool.and_false, Bool.xor_false_right] cases b <;> cases bodd n <;> rfl #align nat.bodd_bit Nat.bodd_bit diff --git a/Mathlib/LinearAlgebra/Orientation.lean b/Mathlib/LinearAlgebra/Orientation.lean index fbd5475426ac4..be1bde9a97bfb 100644 --- a/Mathlib/LinearAlgebra/Orientation.lean +++ b/Mathlib/LinearAlgebra/Orientation.lean @@ -201,7 +201,7 @@ theorem orientation_unitsSMul [Nontrivial R] (e : Basis ι R M) (w : ι → Unit rw [Basis.orientation, Basis.orientation, smul_rayOfNeZero, ray_eq_iff, e.det.eq_smul_basis_det (e.unitsSMul w), det_unitsSMul_self, Units.smul_def, smul_smul] norm_cast - simp + simp only [mul_left_inv, Units.val_one, one_smul] exact SameRay.rfl #align basis.orientation_units_smul Basis.orientation_unitsSMul diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 9708cab144e80..32a545b2ac3c5 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -576,7 +576,7 @@ def linMulLin (f g : M →ₗ[R] R) : QuadraticForm R M where ring exists_companion' := ⟨BilinForm.linMulLin f g + BilinForm.linMulLin g f, fun x y => by - simp + simp only [Pi.mul_apply, map_add, BilinForm.add_apply, BilinForm.linMulLin_apply] ring⟩ #align quadratic_form.lin_mul_lin QuadraticForm.linMulLin diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean index c6467a8845123..f16ccd8d24b91 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean @@ -206,7 +206,9 @@ theorem induction {C : TensorAlgebra R M → Prop} -- the mapping through the subalgebra is the identity have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by ext - simp + simp only [AlgHom.toLinearMap_id, LinearMap.id_comp, AlgHom.comp_toLinearMap, + LinearMap.coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, lift_ι_apply, + Subalgebra.coe_val] erw [LinearMap.codRestrict_apply] -- finding a proof is finding an element of the subalgebra rw [← AlgHom.id_apply (R := R) a, of_id] diff --git a/Mathlib/Logic/Encodable/Lattice.lean b/Mathlib/Logic/Encodable/Lattice.lean index 0b8a9684ed781..3f0652bda21c8 100644 --- a/Mathlib/Logic/Encodable/Lattice.lean +++ b/Mathlib/Logic/Encodable/Lattice.lean @@ -42,7 +42,7 @@ theorem iUnion_decode₂_cases {f : β → Set α} {C : Set α → Prop} (H0 : C C (⋃ b ∈ decode₂ β n, f b) := match decode₂ β n with | none => by - simp + simp only [Option.mem_def, iUnion_of_empty, iUnion_empty] apply H0 | some b => by convert H1 b diff --git a/Mathlib/Logic/Equiv/Option.lean b/Mathlib/Logic/Equiv/Option.lean index 55b8970f65e62..2f2deecd43dee 100644 --- a/Mathlib/Logic/Equiv/Option.lean +++ b/Mathlib/Logic/Equiv/Option.lean @@ -112,8 +112,7 @@ theorem removeNone_aux_inv (x : α) : removeNone_aux e.symm (removeNone_aux e x) · rw [removeNone_aux_some _ ⟨_, h1⟩] rw [removeNone_aux_some _ ⟨_, h2⟩] - simp - ) + simp) -- Porting note: private -- #align equiv.remove_none_aux_inv Equiv.removeNone_aux_inv diff --git a/Mathlib/Logic/Equiv/TransferInstance.lean b/Mathlib/Logic/Equiv/TransferInstance.lean index b4bf13cec962c..93b53e9021d21 100644 --- a/Mathlib/Logic/Equiv/TransferInstance.lean +++ b/Mathlib/Logic/Equiv/TransferInstance.lean @@ -534,7 +534,7 @@ def linearEquiv (e : α ≃ β) [AddCommMonoid β] [Module R β] : by { Equiv.addEquiv e with map_smul' := fun r x => by apply e.symm.injective - simp + simp only [toFun_as_coe_apply, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq] exact Iff.mpr (apply_eq_iff_eq_symm_apply _) rfl } #align equiv.linear_equiv Equiv.linearEquiv diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index 0c594070bbe8a..7cd145992170f 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -1093,7 +1093,7 @@ theorem hausdorffMeasure_smul_right_image [NormedAddCommGroup E] [NormedSpace convert this · simp only [image_smul, LinearMap.toSpanSingleton_apply, Set.image_image] ext e - simp + simp only [mem_image] refine' ⟨fun ⟨x, h⟩ => ⟨x, _⟩, fun ⟨x, h⟩ => ⟨x, _⟩⟩ · rw [smul_comm (norm _), smul_comm (norm _), inv_smul_smul₀ hn] exact h diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean index 47a8d537741f6..424ccbf81a9ab 100644 --- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean @@ -295,7 +295,7 @@ instance instSMul : SMul R (OuterMeasure α) := { measureOf := fun s => c • m s empty := by simp; rw [← smul_one_mul c]; simp mono := fun {s t} h => by - simp + simp only rw [← smul_one_mul c, ← smul_one_mul c (m t)] exact ENNReal.mul_left_mono (m.mono h) iUnion_nat := fun s => by @@ -530,7 +530,7 @@ def comap {β} (f : α → β) : OuterMeasure β →ₗ[ℝ≥0∞] OuterMeasure empty := by simp mono := fun {s t} h => m.mono <| image_subset f h iUnion_nat := fun s => by - simp + simp only rw [image_iUnion] apply m.iUnion_nat } map_add' m₁ m₂ := rfl @@ -682,7 +682,7 @@ protected def ofFunction : OuterMeasure α := intro i apply Subset.trans (hf i).1 apply iUnion_subset - simp + simp only [Nat.pairEquiv_symm_apply] rw [iUnion_unpair] intro j apply subset_iUnion₂ i } @@ -1242,7 +1242,8 @@ theorem map_iInf_comap {ι β} [Nonempty ι] {f : α → β} (m : ι → OuterMe image_preimage_eq_inter_range] exact image_subset _ ht · refine' ENNReal.tsum_le_tsum fun n => iInf_mono fun i => (m i).mono _ - simp + simp only [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty, + image_subset_iff] exact subset_refl _ #align measure_theory.outer_measure.map_infi_comap MeasureTheory.OuterMeasure.map_iInf_comap @@ -1599,7 +1600,7 @@ theorem le_trim : m ≤ m.trim := by apply le_ofFunction.mpr intro s apply le_iInf - simp + simp only [le_refl, implies_true] apply extend_empty <;> simp #align measure_theory.outer_measure.le_trim MeasureTheory.OuterMeasure.le_trim diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean index 7b50ab0f3ee96..e34a6080c8399 100644 --- a/Mathlib/ModelTheory/DirectLimit.lean +++ b/Mathlib/ModelTheory/DirectLimit.lean @@ -295,7 +295,7 @@ def of (i : ι) : G i ↪[L] DirectLimit G f where obtain ⟨j, h1, _, h3⟩ := h exact (f i j h1).injective h3 map_fun' F x := by - simp + simp only rw [← funMap_quotient_mk'_sigma_mk'] rfl map_rel' := by @@ -346,7 +346,7 @@ to a unique map out of the direct limit. -/ def lift : DirectLimit G f ↪[L] P where toFun := Quotient.lift (fun x : Σˣ f => (g x.1) x.2) fun x y xy => by - simp + simp only obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.1 y.1 rw [← Hg x.1 i hx, ← Hg y.1 i hy] exact congr_arg _ ((equiv_iff ..).1 xy) diff --git a/Mathlib/NumberTheory/Dioph.lean b/Mathlib/NumberTheory/Dioph.lean index e9ed059cc35d7..a0fb9cd00e152 100644 --- a/Mathlib/NumberTheory/Dioph.lean +++ b/Mathlib/NumberTheory/Dioph.lean @@ -448,7 +448,7 @@ theorem ex1_dioph {S : Set (Option α → ℕ)} : Dioph S → Dioph {v | ∃ x, ⟨fun ⟨x, hx⟩ => let ⟨t, ht⟩ := (pe _).1 hx ⟨x ::ₒ t, by - simp + simp only [Poly.map_apply] rw [show (v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = x ::ₒ v ⊗ t from funext fun s => by cases' s with a b <;> try { cases a <;> rfl}; rfl] exact ht⟩, @@ -545,7 +545,7 @@ theorem diophFn_compn : ext x; obtain _ | _ | _ := x; rfl | succ n, S, d, f => f.consElim fun f fl => by - simp + simp only [vectorAllP_cons, and_imp] exact fun df dfl => have : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl)::v ∘ inr) ∈ S} := ext (diophFn_comp1 (reindex_dioph _ (some ∘ inl ⊗ none::some ∘ inr) d) <| @@ -572,7 +572,7 @@ theorem dioph_comp {S : Set (Vector3 ℕ n)} (d : Dioph S) (f : Vector3 ((α → theorem diophFn_comp {f : Vector3 ℕ n → ℕ} (df : DiophFn f) (g : Vector3 ((α → ℕ) → ℕ) n) (dg : VectorAllP DiophFn g) : DiophFn fun v => f fun i => g i v := dioph_comp ((diophFn_vec _).1 df) ((fun v => v none)::fun i v => g i (v ∘ some)) <| by - simp + simp only [vectorAllP_cons] exact ⟨proj_dioph none, (vectorAllP_iff_forall _ _).2 fun i => reindex_diophFn _ <| (vectorAllP_iff_forall _ _).1 dg _⟩ #align dioph.dioph_fn_comp Dioph.diophFn_comp diff --git a/Mathlib/NumberTheory/Zsqrtd/Basic.lean b/Mathlib/NumberTheory/Zsqrtd/Basic.lean index 938301724516d..340c91583e0ae 100644 --- a/Mathlib/NumberTheory/Zsqrtd/Basic.lean +++ b/Mathlib/NumberTheory/Zsqrtd/Basic.lean @@ -1040,7 +1040,7 @@ def lift {d : ℤ} : { r : R // r * r = ↑d } ≃ (ℤ√d →+* R) where { toFun := fun a => a.1 + a.2 * (r : R) map_zero' := by simp map_add' := fun a b => by - simp + simp only [add_re, Int.cast_add, add_im] ring map_one' := by simp map_mul' := fun a b => by diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 741ec77840228..23f6b1bda86ac 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -1265,7 +1265,7 @@ def lift.principalSeg : @PrincipalSeg Ordinal.{u} Ordinal.{max (u + 1) v} (· < · intro a' cases' (hf _).1 (typein_lt_type _ a') with b e exists b - simp + simp only [RelEmbedding.ofMonotone_coe] simp [e] · cases' h with a e rw [← e] diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index 7ab0d5366b00f..3bf62af6580c4 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -719,7 +719,8 @@ theorem split_eq_scale_split' : ∀ {o o' m} [NF o], split' o = (o', m) → spli simp [split_eq_scale_split' h', split, split'] have : 1 + (e - 1) = e := by refine' repr_inj.1 _ - simp + simp only [repr_add, repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, add_zero, + repr_sub] have := mt repr_inj.1 e0 refine' Ordinal.add_sub_cancel_of_le _ have := (one_le_iff_ne_zero.2 this) diff --git a/Mathlib/Topology/Algebra/ValuedField.lean b/Mathlib/Topology/Algebra/ValuedField.lean index 490c8d033390f..7a19dbd9af9f4 100644 --- a/Mathlib/Topology/Algebra/ValuedField.lean +++ b/Mathlib/Topology/Algebra/ValuedField.lean @@ -287,7 +287,7 @@ noncomputable def extensionValuation : Valuation (hat K) Γ₀ where rw [← v.map_zero (R := K), ← Valued.extension_extends (0 : K)] rfl map_one' := by - simp + simp only rw [← Completion.coe_one, Valued.extension_extends (1 : K)] exact Valuation.map_one _ map_mul' x y := by