From 0861c664e8d2afef476e0722a9bd73a2f39fa964 Mon Sep 17 00:00:00 2001 From: grunweg Date: Wed, 20 Mar 2024 13:56:13 +0000 Subject: [PATCH] golf: replace some `apply foo.mpr` by `rw [foo]` (#11515) Sometimes, that line can be golfed into the next line. Inspired by a [comment](https://github.com/leanprover-community/mathlib4/pull/11208#discussion_r1530467335) of @loefflerd; any decisions are my own. --- Mathlib/Algebra/BigOperators/Basic.lean | 3 +-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 4 ++-- Mathlib/Analysis/NormedSpace/Units.lean | 2 +- Mathlib/Control/Functor/Multivariate.lean | 2 +- Mathlib/Data/BitVec/Lemmas.lean | 4 ++-- Mathlib/Data/List/Nodup.lean | 2 +- Mathlib/Data/List/Pairwise.lean | 4 ++-- Mathlib/Data/Set/Intervals/Disjoint.lean | 5 ++--- Mathlib/FieldTheory/PrimitiveElement.lean | 2 +- Mathlib/Geometry/Manifold/ChartedSpace.lean | 2 +- Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean | 4 ++-- Mathlib/GroupTheory/NoncommPiCoprod.lean | 2 +- Mathlib/Logic/Equiv/Defs.lean | 4 ++-- Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean | 2 +- Mathlib/Topology/ContinuousFunction/Weierstrass.lean | 2 +- Mathlib/Topology/EMetricSpace/Lipschitz.lean | 2 +- 16 files changed, 22 insertions(+), 24 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 98c2a38a31d0e..2cef2415b2fa0 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -977,8 +977,7 @@ theorem prod_eq_mul_of_mem {s : Finset α} {f : α → β} (a b : α) (ha : a apply not_or.mp intro hab apply hcs - apply mem_insert.mpr - rw [mem_singleton] + rw [mem_insert, mem_singleton] exact hab rw [← prod_subset hu hf] exact Finset.prod_pair hn diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index fc0dbf40fd5d8..0f99d7f5af3b9 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -1765,7 +1765,7 @@ theorem contDiffAt_ring_inverse [CompleteSpace R] (x : Rˣ) : · rintro _ ⟨x', rfl⟩ exact (inverse_continuousAt x').continuousWithinAt · simp [ftaylorSeriesWithin] - · apply contDiffAt_succ_iff_hasFDerivAt.mpr + · rw [contDiffAt_succ_iff_hasFDerivAt] refine' ⟨fun x : R => -mulLeftRight 𝕜 R (inverse x) (inverse x), _, _⟩ · refine' ⟨{ y : R | IsUnit y }, x.nhds, _⟩ rintro _ ⟨y, rfl⟩ @@ -1883,7 +1883,7 @@ theorem PartialHomeomorph.contDiffAt_symm [CompleteSpace E] (f : PartialHomeomor · rw [contDiffAt_zero] exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩ · obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf - apply contDiffAt_succ_iff_hasFDerivAt.mpr + rw [contDiffAt_succ_iff_hasFDerivAt] -- For showing `n.succ` times continuous differentiability (the main inductive step), it -- suffices to produce the derivative and show that it is `n` times continuously differentiable have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀' diff --git a/Mathlib/Analysis/NormedSpace/Units.lean b/Mathlib/Analysis/NormedSpace/Units.lean index 77dff40dd1525..5489878814ed0 100644 --- a/Mathlib/Analysis/NormedSpace/Units.lean +++ b/Mathlib/Analysis/NormedSpace/Units.lean @@ -76,7 +76,7 @@ def ofNearby (x : Rˣ) (y : R) (h : ‖y - x‖ < ‖(↑x⁻¹ : R)‖⁻¹) : /-- The group of units of a complete normed ring is an open subset of the ring. -/ protected theorem isOpen : IsOpen { x : R | IsUnit x } := by nontriviality R - apply Metric.isOpen_iff.mpr + rw [Metric.isOpen_iff] rintro _ ⟨x, rfl⟩ refine' ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ _⟩ rw [mem_ball_iff_norm] at hy diff --git a/Mathlib/Control/Functor/Multivariate.lean b/Mathlib/Control/Functor/Multivariate.lean index 10420cf185cf3..738e8b422c817 100644 --- a/Mathlib/Control/Functor/Multivariate.lean +++ b/Mathlib/Control/Functor/Multivariate.lean @@ -128,7 +128,7 @@ theorem exists_iff_exists_of_mono {P : F α → Prop} {q : F β → Prop} · refine ⟨f <$$> u, ?_⟩ apply (h₁ u).mp h₂ · refine ⟨g <$$> u, ?_⟩ - apply (h₁ _).mpr _ + rw [h₁] simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂] #align mvfunctor.exists_iff_exists_of_mono MvFunctor.exists_iff_exists_of_mono diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 55c9949a3dc0c..64c4d2c2f69c8 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -166,14 +166,14 @@ variable (x y : BitVec w) -- These should be simp, but Std's simp-lemmas do not allow this yet. lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl lemma toFin_one : toFin (1 : BitVec w) = 1 := by - apply toFin_inj.mpr; simp only [ofNat_eq_ofNat, ofFin_ofNat] + rw [toFin_inj]; simp only [ofNat_eq_ofNat, ofFin_ofNat] lemma toFin_nsmul (n : ℕ) (x : BitVec w) : toFin (n • x) = n • x.toFin := rfl lemma toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin := rfl @[simp] lemma toFin_pow (n : ℕ) : toFin (x ^ n) = x.toFin ^ n := rfl lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n := by - apply toFin_inj.mpr; simp only [ofFin_natCast] + rw [toFin_inj]; simp only [ofFin_natCast] end diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean index 2c31b807459b4..9e115e822bf47 100644 --- a/Mathlib/Data/List/Nodup.lean +++ b/Mathlib/Data/List/Nodup.lean @@ -441,7 +441,7 @@ theorem Nodup.map_update [DecidableEq α] {l : List α} (hl : l.Nodup) (f : α theorem Nodup.pairwise_of_forall_ne {l : List α} {r : α → α → Prop} (hl : l.Nodup) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by - apply pairwise_iff_forall_sublist.mpr + rw [pairwise_iff_forall_sublist] intro a b hab if heq : a = b then cases heq; have := nodup_iff_sublist.mp hl _ hab; contradiction diff --git a/Mathlib/Data/List/Pairwise.lean b/Mathlib/Data/List/Pairwise.lean index 949d14837bca1..2446643894963 100644 --- a/Mathlib/Data/List/Pairwise.lean +++ b/Mathlib/Data/List/Pairwise.lean @@ -151,14 +151,14 @@ theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h : ∀ a ∈ l, ∀ b ∈ l, r a b) : l.Pairwise r := by - apply pairwise_iff_forall_sublist.mpr + rw [pairwise_iff_forall_sublist] intro a b hab apply h <;> (apply hab.subset; simp) #align list.pairwise_of_forall_mem_list List.pairwise_of_forall_mem_list theorem pairwise_of_reflexive_of_forall_ne {l : List α} {r : α → α → Prop} (hr : Reflexive r) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by - apply pairwise_iff_forall_sublist.mpr + rw [pairwise_iff_forall_sublist] intro a b hab if heq : a = b then cases heq; apply hr diff --git a/Mathlib/Data/Set/Intervals/Disjoint.lean b/Mathlib/Data/Set/Intervals/Disjoint.lean index 0ff692048f52c..345f016e45d75 100644 --- a/Mathlib/Data/Set/Intervals/Disjoint.lean +++ b/Mathlib/Data/Set/Intervals/Disjoint.lean @@ -214,7 +214,7 @@ theorem IsGLB.biUnion_Ici_eq_Ioi (a_glb : IsGLB s a) (a_not_mem : a ∉ s) : refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _ · exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_not_mem) hx) · rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩ - apply mem_iUnion₂.mpr + rw [mem_iUnion₂] exact ⟨y, hys, hyx.le⟩ #align is_glb.bUnion_Ici_eq_Ioi IsGLB.biUnion_Ici_eq_Ioi @@ -222,8 +222,7 @@ theorem IsGLB.biUnion_Ici_eq_Ici (a_glb : IsGLB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Ici x = Ici a := by refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _ · exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx) - · apply mem_iUnion₂.mpr - exact ⟨a, a_mem, hx⟩ + · exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩ #align is_glb.bUnion_Ici_eq_Ici IsGLB.biUnion_Ici_eq_Ici theorem IsLUB.biUnion_Iic_eq_Iio (a_lub : IsLUB s a) (a_not_mem : a ∉ s) : diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean index 689be17e868f4..4a1ed197dd91a 100644 --- a/Mathlib/FieldTheory/PrimitiveElement.lean +++ b/Mathlib/FieldTheory/PrimitiveElement.lean @@ -56,7 +56,7 @@ variable (F : Type*) [Field F] (E : Type*) [Field E] [Algebra F E] theorem exists_primitive_element_of_finite_top [Finite E] : ∃ α : E, F⟮α⟯ = ⊤ := by obtain ⟨α, hα⟩ := @IsCyclic.exists_generator Eˣ _ _ use α - apply eq_top_iff.mpr + rw [eq_top_iff] rintro x - by_cases hx : x = 0 · rw [hx] diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index 94ec2cd0b839b..cd42d31a7cbbd 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -513,7 +513,7 @@ theorem closedUnderRestriction_iff_id_le (G : StructureGroupoid H) : ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G := by constructor · intro _i - apply StructureGroupoid.le_iff.mpr + rw [StructureGroupoid.le_iff] rintro e ⟨s, hs, hes⟩ refine' G.mem_of_eqOnSource _ hes convert closedUnderRestriction' G.id_mem hs diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index 6303a4b91352d..906ae82dcab7d 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -652,7 +652,7 @@ theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCor instance : ClosedUnderRestriction (contDiffGroupoid n I) := (closedUnderRestriction_iff_id_le _).mpr (by - apply StructureGroupoid.le_iff.mpr + rw [StructureGroupoid.le_iff] rintro e ⟨s, hs, hes⟩ apply (contDiffGroupoid n I).mem_of_eqOnSource' _ _ _ hes exact ofSet_mem_contDiffGroupoid n I hs) @@ -790,7 +790,7 @@ theorem symm_trans_mem_analyticGroupoid (e : PartialHomeomorph M H) : instance : ClosedUnderRestriction (analyticGroupoid I) := (closedUnderRestriction_iff_id_le _).mpr (by - apply StructureGroupoid.le_iff.mpr + rw [StructureGroupoid.le_iff] rintro e ⟨s, hs, hes⟩ apply (analyticGroupoid I).mem_of_eqOnSource' _ _ _ hes exact ofSet_mem_analyticGroupoid I hs) diff --git a/Mathlib/GroupTheory/NoncommPiCoprod.lean b/Mathlib/GroupTheory/NoncommPiCoprod.lean index 32fac9ec23d4d..765164c02b70c 100644 --- a/Mathlib/GroupTheory/NoncommPiCoprod.lean +++ b/Mathlib/GroupTheory/NoncommPiCoprod.lean @@ -213,7 +213,7 @@ theorem injective_noncommPiCoprod_of_independent (hinj : ∀ i, Function.Injective (ϕ i)) : Function.Injective (noncommPiCoprod ϕ hcomm) := by classical apply (MonoidHom.ker_eq_bot_iff _).mp - apply eq_bot_iff.mpr + rw [eq_bot_iff] intro f heq1 have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 := Subgroup.eq_one_of_noncommProd_eq_one_of_independent _ _ (fun _ _ _ _ h => hcomm h _ _) diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean index 267bee15b11c6..24232c6dc3a5d 100644 --- a/Mathlib/Logic/Equiv/Defs.lean +++ b/Mathlib/Logic/Equiv/Defs.lean @@ -886,8 +886,8 @@ protected theorem exists_unique_congr_left {p : β → Prop} (f : α ≃ β) : protected theorem forall_congr {p : α → Prop} {q : β → Prop} (f : α ≃ β) (h : ∀ {x}, p x ↔ q (f x)) : (∀ x, p x) ↔ (∀ y, q y) := by constructor <;> intro h₂ x - · rw [← f.right_inv x]; apply h.mp; apply h₂ - · apply h.mpr; apply h₂ + · rw [← f.right_inv x]; exact h.mp (h₂ _) + · exact h.mpr (h₂ _) #align equiv.forall_congr Equiv.forall_congr protected theorem forall_congr' {p : α → Prop} {q : β → Prop} (f : α ≃ β) diff --git a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean index e617cfe757167..78417390eec22 100644 --- a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean +++ b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean @@ -171,7 +171,7 @@ theorem sublattice_closure_eq_top (L : Set C(X, ℝ)) (nA : L.Nonempty) (sup_mem : ∀ᵉ (f ∈ L) (g ∈ L), f ⊔ g ∈ L) (sep : L.SeparatesPointsStrongly) : closure L = ⊤ := by -- We start by boiling down to a statement about close approximation. - apply eq_top_iff.mpr + rw [eq_top_iff] rintro f - refine' Filter.Frequently.mem_closure diff --git a/Mathlib/Topology/ContinuousFunction/Weierstrass.lean b/Mathlib/Topology/ContinuousFunction/Weierstrass.lean index ec1468619e374..7c65e4d860e20 100644 --- a/Mathlib/Topology/ContinuousFunction/Weierstrass.lean +++ b/Mathlib/Topology/ContinuousFunction/Weierstrass.lean @@ -30,7 +30,7 @@ open scoped unitInterval This is just a matter of unravelling definitions and using the Bernstein approximations. -/ theorem polynomialFunctions_closure_eq_top' : (polynomialFunctions I).topologicalClosure = ⊤ := by - apply eq_top_iff.mpr + rw [eq_top_iff] rintro f - refine' Filter.Frequently.mem_closure _ refine' Filter.Tendsto.frequently (bernsteinApproximation_uniform f) _ diff --git a/Mathlib/Topology/EMetricSpace/Lipschitz.lean b/Mathlib/Topology/EMetricSpace/Lipschitz.lean index 3ddfafc02d168..f30dfa5a85f51 100644 --- a/Mathlib/Topology/EMetricSpace/Lipschitz.lean +++ b/Mathlib/Topology/EMetricSpace/Lipschitz.lean @@ -364,7 +364,7 @@ protected lemma const (b : β) : LocallyLipschitz (fun _ : α ↦ b) := /-- A locally Lipschitz function is continuous. (The converse is false: for example, $x ↦ \sqrt{x}$ is continuous, but not locally Lipschitz at 0.) -/ protected theorem continuous {f : α → β} (hf : LocallyLipschitz f) : Continuous f := by - apply continuous_iff_continuousAt.mpr + rw [continuous_iff_continuousAt] intro x rcases (hf x) with ⟨K, t, ht, hK⟩ exact (hK.continuousOn).continuousAt ht