diff --git a/Mathlib/Algebra/Lie/Weights/Cartan.lean b/Mathlib/Algebra/Lie/Weights/Cartan.lean
index ac6795709a85ac..e6da1b44287b17 100644
--- a/Mathlib/Algebra/Lie/Weights/Cartan.lean
+++ b/Mathlib/Algebra/Lie/Weights/Cartan.lean
@@ -330,7 +330,7 @@ lemma lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace (I : LieIdeal K L) :
   conv_lhs => rw [lieIdeal_eq_iSup_inf_genWeightSpace]
   exact iSup_le fun α ↦ by
     by_cases hα : α.IsZero
-    · rw [show genWeightSpace L (α : H → K) = H.toLieSubmodule from by ext; simp [hα.eq]]
+    · rw [show genWeightSpace L (α : H → K) = H.toLieSubmodule by ext; simp [hα.eq]]
       exact le_sup_left
     · exact le_sup_of_le_right (le_iSup₂_of_le α hα le_rfl)
 
diff --git a/Mathlib/Analysis/Convex/Approximation.lean b/Mathlib/Analysis/Convex/Approximation.lean
index cd2fd270b26db8..1e2ae788358a8d 100644
--- a/Mathlib/Analysis/Convex/Approximation.lean
+++ b/Mathlib/Analysis/Convex/Approximation.lean
@@ -115,7 +115,7 @@ theorem sSup_affine_eq (hsc : IsClosed s)
   ext x
   rw [sSup_apply]
   refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ (fun r ⟨f, hf⟩ => ?_) (fun r hr => ?_)
-  · obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) x.2 (show φ x - 1 < φ x from by grind)
+  · obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) x.2 (show φ x - 1 < φ x by grind)
       hsc hφc hφcv
     exact ⟨φ x - 1, hlc.2 ▸ ⟨⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩⟩
   · exact hf ▸ f.2.1 x
diff --git a/Mathlib/Analysis/MeanInequalitiesPow.lean b/Mathlib/Analysis/MeanInequalitiesPow.lean
index d157730b07294d..18b89c5d8dbae4 100644
--- a/Mathlib/Analysis/MeanInequalitiesPow.lean
+++ b/Mathlib/Analysis/MeanInequalitiesPow.lean
@@ -351,7 +351,7 @@ theorem rpow_add_le_mul_rpow_add_rpow' (z₁ z₂ : ℝ≥0∞) {p : ℝ} (hp :
       · simp
       · rwa [ENNReal.inv_lt_one, one_lt_ofReal]
     rw [show LpAddConst (ENNReal.ofReal p)⁻¹ =
-        (2 : ℝ≥0∞) ^ (1 / ((ENNReal.ofReal p)⁻¹).toReal - 1) from by
+        (2 : ℝ≥0∞) ^ (1 / ((ENNReal.ofReal p)⁻¹).toReal - 1) by
       rw [LpAddConst, if_pos hmem]]
     simp only [ENNReal.toReal_inv, div_inv_eq_mul, one_mul]
     rw [ENNReal.toReal_ofReal hp]
diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean
index 71d466e6a1089c..d5261c5c7fdc98 100644
--- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean
+++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean
@@ -352,7 +352,7 @@ root of its degree plus one. -/
 theorem mahlerMeasure_le_sqrt_natDegree_add_one_mul_supNorm (p : Polynomial ℂ) :
     p.mahlerMeasure ≤ √(p.natDegree + 1) * p.supNorm :=
   (p.mahlerMeasure_le_sqrt_sum_sq_norm_coeff).trans <| by
-    rw [show √(↑(p.natDegree) + 1) * p.supNorm = √((p.natDegree + 1) * p.supNorm ^ 2) from by
+    rw [show √(↑(p.natDegree) + 1) * p.supNorm = √((p.natDegree + 1) * p.supNorm ^ 2) by
       rw [Real.sqrt_mul (by positivity), Real.sqrt_sq p.supNorm_nonneg]]
     gcongr
     refine (p.support.sum_le_card_nsmul _ (p.supNorm ^ 2) fun i _ ↦ ?_).trans ?_
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
index 917b893f1dbf0f..db670cce839bd2 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
@@ -89,7 +89,7 @@ def isLimitPullbackConeMapOfIsLimit [PreservesLimit (cospan f g) G]
 /-- The property of reflecting pullbacks expressed in terms of binary fans. -/
 def isLimitOfIsLimitPullbackConeMap [ReflectsLimit (cospan f g) G]
     (l : IsLimit (PullbackCone.mk (G.map h) (G.map k) (show G.map h ≫ G.map f = G.map k ≫ G.map g
-    from by simp only [← G.map_comp, comm]))) : IsLimit (PullbackCone.mk h k comm) :=
+    by simp only [← G.map_comp, comm]))) : IsLimit (PullbackCone.mk h k comm) :=
   isLimitOfReflects G
     ((PullbackCone.isLimitMapConeEquiv (PullbackCone.mk _ _ comm) G).2 l)
 
@@ -222,7 +222,7 @@ def isColimitPushoutCoconeMapOfIsColimit [PreservesColimit (span f g) G]
 /-- The property of reflecting pushouts expressed in terms of binary cofans. -/
 def isColimitOfIsColimitPushoutCoconeMap [ReflectsColimit (span f g) G]
     (l : IsColimit (PushoutCocone.mk (G.map h) (G.map k) (show G.map f ≫ G.map h =
-      G.map g ≫ G.map k from by simp only [← G.map_comp, comm]))) :
+      G.map g ≫ G.map k by simp only [← G.map_comp, comm]))) :
     IsColimit (PushoutCocone.mk h k comm) :=
   isColimitOfReflects G ((isColimitMapCoconePushoutCoconeEquiv G comm).symm l)
 
@@ -232,7 +232,7 @@ variable (f g) [PreservesColimit (span f g) G]
 morphisms of the pushout cocone is a colimit. -/
 def isColimitOfHasPushoutOfPreservesColimit [i : HasPushout f g] :
     IsColimit (PushoutCocone.mk (G.map (pushout.inl _ _)) (G.map (@pushout.inr _ _ _ _ _ f g i))
-    (show G.map f ≫ G.map (pushout.inl _ _) = G.map g ≫ G.map (pushout.inr _ _) from by
+    (show G.map f ≫ G.map (pushout.inl _ _) = G.map g ≫ G.map (pushout.inr _ _) by
       simp only [← G.map_comp, pushout.condition])) :=
   isColimitPushoutCoconeMapOfIsColimit G _ (pushoutIsPushout f g)
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
index 705894aae5d3af..31af169e54f790 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
@@ -323,7 +323,7 @@ instance epi_coprod_to_pushout {C : Type*} [Category* C] {X Y Z : C} (f : X ⟶
 /-- The pushout of `f, g` is also the pullback of `h ≫ f, h ≫ g` for any epi `h`. -/
 noncomputable def pushoutIsPushoutOfEpiComp (f : X ⟶ Y) (g : X ⟶ Z) (h : W ⟶ X) [Epi h]
     [HasPushout f g] : IsColimit (PushoutCocone.mk (pushout.inl f g) (pushout.inr f g)
-    (show (h ≫ f) ≫ pushout.inl f g = (h ≫ g) ≫ pushout.inr f g from by
+    (show (h ≫ f) ≫ pushout.inl f g = (h ≫ g) ≫ pushout.inr f g by
     simp only [Category.assoc]; rw [cancel_epi]; exact pushout.condition)) :=
   PushoutCocone.isColimitOfEpiComp f g h _ (colimit.isColimit (span f g))
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
index aac973d31a57db..5d25f8c3a90171 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
@@ -278,7 +278,7 @@ theorem toSubgraph_adj_snd {u v} (w : G.Walk u v) (h : ¬ w.Nil) : w.toSubgraph.
 theorem toSubgraph_adj_penultimate {u v} (w : G.Walk u v) (h : ¬ w.Nil) :
     w.toSubgraph.Adj w.penultimate v := by
   rw [not_nil_iff_lt_length] at h
-  simpa [show w.length - 1 + 1 = w.length from by lia]
+  simpa [show w.length - 1 + 1 = w.length by lia]
     using w.toSubgraph_adj_getVert (by lia : w.length - 1 < w.length)
 
 theorem toSubgraph_adj_iff {u v u' v'} (w : G.Walk u v) :
@@ -391,7 +391,7 @@ lemma neighborSet_toSubgraph_endpoint {u v} {p : G.Walk u v}
 lemma neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath)
     (h : i ≠ 0) (h' : i < p.length) :
     p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)} := by
-  have hadj1 := ((show i - 1 + 1 = i from by lia) ▸
+  have hadj1 := ((show i - 1 + 1 = i by lia) ▸
     p.toSubgraph_adj_getVert (by lia : (i - 1) < p.length)).symm
   ext v
   simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
@@ -441,7 +441,7 @@ lemma neighborSet_toSubgraph_endpoint {u} {p : G.Walk u u} (hpc : p.IsCycle) :
 lemma neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle)
     (h : i ≠ 0) (h' : i < p.length) :
     p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)} := by
-  have hadj1 := ((show i - 1 + 1 = i from by lia) ▸
+  have hadj1 := ((show i - 1 + 1 = i by lia) ▸
     p.toSubgraph_adj_getVert (by lia : (i - 1) < p.length)).symm
   ext v
   simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
diff --git a/Mathlib/Combinatorics/SimpleGraph/Matching.lean b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
index 376f0441c1051e..87b8654c30b185 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Matching.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
@@ -519,7 +519,7 @@ lemma IsCycles.reachable_deleteEdges [Finite V] (hadj : G.Adj v w)
     simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
       Set.mem_singleton_iff, or_true, sup_of_le_left]
     exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm
-  rw [show G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)} from by rfl]
+  rw [show G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)} by rfl]
   exact this ▸ (hcyc.reachable_sdiff_toSubgraph_spanningCoe hadj.toWalk
     (Walk.IsPath.of_adj hadj)).symm
 
@@ -613,14 +613,14 @@ lemma Subgraph.IsPerfectMatching.symmDiff_of_isAlternating (hM : M.IsPerfectMatc
     · grind
     · obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1
       by_contra! hc
-      simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hc hr.1 hw'.2]
+      simp_all [show M.Adj v y ↔ ¬M.Adj v w' by simpa using hG' hc hr.1 hw'.2]
   · use w
     simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hw.1, h,
       not_false_eq_true, and_self, not_true_eq_false, or_false, true_and]
     rintro y (hl | hr)
     · exact hw.2 _ hl.1
     · have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1
-      simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hw'.1 hr.1 hw'.2]
+      simp_all [show M.Adj v y ↔ ¬M.Adj v w' by simpa using hG' hw'.1 hr.1 hw'.2]
 
 lemma Subgraph.IsPerfectMatching.isAlternating_symmDiff_left {M' : Subgraph G'}
     (hM : M.IsPerfectMatching) (hM' : M'.IsPerfectMatching) :
diff --git a/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean b/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
index 28ff818b96ad57..d80e862c7214c6 100644
--- a/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
+++ b/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
@@ -200,7 +200,7 @@ theorem isMultiplyPreprimitive_succ_iff_ofStabilizer
       simp only
       rw [← Nat.cast_one, ← Nat.cast_add, ← hs]
       apply congr_arg₂ _ _ rfl
-      rw [show s = g⁻¹ • s' from by simp [hs'],
+      rw [show s = g⁻¹ • s' by simp [hs'],
         ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]
       rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, ENat.coe_one]
       exact notMem_val_image M t
diff --git a/Mathlib/LinearAlgebra/JordanChevalley.lean b/Mathlib/LinearAlgebra/JordanChevalley.lean
index 49f61b5a236dbe..cfea752c5ae0eb 100644
--- a/Mathlib/LinearAlgebra/JordanChevalley.lean
+++ b/Mathlib/LinearAlgebra/JordanChevalley.lean
@@ -94,7 +94,7 @@ theorem isNilpotent_isSemisimple_unique [PerfectField K]
   have hsf : Commute s (n₁ + s₁) := heq ▸ hc.symm.add_right (Commute.refl s)
   have hnf : Commute n (n₁ + s₁) := heq ▸ (Commute.refl n).add_right hc
   have hnil : IsNilpotent (s - s₀) := by
-    rw [show s - s₀ = n₀ - n from by grind]
+    rw [show s - s₀ = n₀ - n by grind]
     exact (commute_of_mem_adjoin_singleton_of_commute hn₀ hnf).symm.isNilpotent_sub hn₀_nil hn
   have hss : (s - s₀).IsSemisimple :=
     hs.sub_of_commute (commute_of_mem_adjoin_singleton_of_commute hs₀ hsf) hs₀_ss
diff --git a/Mathlib/LinearAlgebra/Projectivization/Action.lean b/Mathlib/LinearAlgebra/Projectivization/Action.lean
index 7ff05dfca850b4..4b1cbe2b8ea2a1 100644
--- a/Mathlib/LinearAlgebra/Projectivization/Action.lean
+++ b/Mathlib/LinearAlgebra/Projectivization/Action.lean
@@ -146,7 +146,7 @@ instance specialLinearGroup_is_two_pretransitive :
       suffices (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1 by
         rw [this, Module.Basis.extend_apply_self, Units.smul_def]
         module
-      nth_rewrite 1 [show D.rep = (⟨D.rep, hD_mem⟩ : s) from by rfl]
+      nth_rewrite 1 [show D.rep = (⟨D.rep, hD_mem⟩ : s) by rfl]
       rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
       simp
     · rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]
@@ -156,7 +156,7 @@ instance specialLinearGroup_is_two_pretransitive :
       suffices (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0 by
         rw [Module.Basis.extend_apply_self]
         simp [this]
-      nth_rewrite 1 [show D'.rep = (⟨D'.rep, hD'_mem⟩ : s) from by rfl]
+      nth_rewrite 1 [show D'.rep = (⟨D'.rep, hD'_mem⟩ : s) by rfl]
       rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
       apply Finsupp.single_eq_of_ne
       simp only [ne_eq, ← Subtype.coe_inj]
diff --git a/Mathlib/RingTheory/HopfAlgebra/Convolution.lean b/Mathlib/RingTheory/HopfAlgebra/Convolution.lean
index ef72940b1e6023..aae1f434c68830 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Convolution.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Convolution.lean
@@ -115,7 +115,7 @@ lemma comul_right_inv : toConv δ * toConv 𝑭 = 1 := by
     _ = δ ∘ₗ (toConv id * toConv 𝑺).ofConv := by simp [LinearMap.convMul_def]
     _ = δ ∘ₗ (1 : WithConv (C →ₗ[R] C)).ofConv := by rw [id_mul_antipode]
     _ = η ∘ₗ ε := by
-        simp [LinearMap.convOne_def, show (δ ∘ₗ η : R →ₗ[R] C ⊗[R] C) = η from by ext; simp; rfl,
+        simp [LinearMap.convOne_def, show (δ ∘ₗ η : R →ₗ[R] C ⊗[R] C) = η by ext; simp; rfl,
           ← comp_assoc]
 
 end LinearMap
diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean
index b175611ea822d6..fc1387005e15c0 100644
--- a/Mathlib/Topology/Algebra/Monoid.lean
+++ b/Mathlib/Topology/Algebra/Monoid.lean
@@ -90,8 +90,8 @@ instance ContinuousMul.to_continuousSMul : ContinuousSMul M M :=
 
 @[to_additive]
 instance ContinuousMul.to_continuousSMul_op : ContinuousSMul Mᵐᵒᵖ M :=
-  ⟨show Continuous ((fun p : M × M => p.1 * p.2) ∘ Prod.swap ∘ Prod.map MulOpposite.unop id) from
-    by fun_prop⟩
+  ⟨show Continuous ((fun p : M × M => p.1 * p.2) ∘ Prod.swap ∘ Prod.map MulOpposite.unop id) by
+    fun_prop⟩
 
 @[to_additive]
 theorem ContinuousMul.induced {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Mul α]
diff --git a/Mathlib/Topology/Compactification/OnePoint/Basic.lean b/Mathlib/Topology/Compactification/OnePoint/Basic.lean
index 2640e0361b0fa5..ed57d3affd569b 100644
--- a/Mathlib/Topology/Compactification/OnePoint/Basic.lean
+++ b/Mathlib/Topology/Compactification/OnePoint/Basic.lean
@@ -589,7 +589,7 @@ noncomputable def equivOfIsEmbeddingOfRangeEq :
     exact (isClosed_compl_iff.mpr hU₂).isCompact
   let e : OnePoint X ≃ Y :=
     { toFun := fun p ↦ p.elim y f
-      invFun := fun q ↦ if hq : q = y then ∞ else ↑(show q ∈ range f from by simpa [hy]).choose
+      invFun := fun q ↦ if hq : q = y then ∞ else ↑(show q ∈ range f by simpa [hy]).choose
       left_inv := fun p ↦ by
         induction p using OnePoint.rec with
         | infty => simp