chore: tidy various files (#11624)

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -573,7 +573,7 @@ theorem cannot_cube_a_cube :
     ∀ {s : Set (Cube n)}, s.Finite →           -- given a finite collection of (hyper)cubes
     s.Nontrivial →                             -- containing at least two elements
     s.PairwiseDisjoint Cube.toSet →            -- which is pairwise disjoint
-    ⋃ c ∈ s, Cube.toSet c = unitCube.toSet → -- whose union is the unit cube
+    ⋃ c ∈ s, Cube.toSet c = unitCube.toSet →   -- whose union is the unit cube
     InjOn Cube.w s →                           -- such that the widths of all cubes are different
     False := by                                -- then we can derive a contradiction
   intro n hn s hfin h2 hd hU hinj

Mathlib/Algebra/Divisibility/Units.lean

@@ -251,8 +251,9 @@ theorem IsRelPrime.mul_left (H1 : IsRelPrime x z) (H2 : IsRelPrime y z) : IsRelP
     obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h
     exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)
 
-theorem IsRelPrime.mul_right (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) : IsRelPrime x (y * z) :=
-  by rw [isRelPrime_comm] at H1 H2 ⊢; exact H1.mul_left H2
+theorem IsRelPrime.mul_right (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) :
+    IsRelPrime x (y * z) := by
+  rw [isRelPrime_comm] at H1 H2 ⊢; exact H1.mul_left H2
 
 theorem IsRelPrime.mul_left_iff : IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z :=
   ⟨fun H ↦ ⟨H.of_mul_left_left, H.of_mul_left_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_left H2⟩

Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

@@ -25,7 +25,7 @@ namespace Submodule
 variable (S : Type*) {R M : Type*} [Semiring R] [AddCommMonoid M] [Semiring S]
   [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M]
 
-/-- `V.restrict_scalars S` is the `S`-submodule of the `S`-module given by restriction of scalars,
+/-- `V.restrictScalars S` is the `S`-submodule of the `S`-module given by restriction of scalars,
 corresponding to `V`, an `R`-submodule of the original `R`-module.
 -/
 def restrictScalars (V : Submodule R M) : Submodule S M where

Mathlib/Algebra/Order/Monoid/MinMax.lean

@@ -21,7 +21,7 @@ variable {α β : Type*}
   rules relating them. -/
 
 section CommSemigroup
-variable[LinearOrder α] [CommSemigroup α] [CommSemigroup β]
+variable [LinearOrder α] [CommSemigroup α] [CommSemigroup β]
 
 @[to_additive]
 lemma fn_min_mul_fn_max  (f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b := by

Mathlib/Algebra/Ring/InjSurj.lean

@@ -304,7 +304,7 @@ protected def Function.Injective.commSemiring [CommSemiring α] (f : β → α)
   __ := hf.commSemigroup f mul
 #align function.injective.comm_semiring Function.Injective.commSemiring
 
-/-- Pushforward a `NonAssocSemiring` instance along a surjective function. -/
+/-- Pushforward a `CommSemiring` instance along a surjective function. -/
 @[reducible] -- See note [reducible non-instances]
 protected def Function.Surjective.commSemiring [CommSemiring α] (f : α → β) (hf : Surjective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -569,9 +569,7 @@ theorem basicOpen_union_eq_self_iff (s : Set (X.presheaf.obj <| op U)) :
     intro x _
     exact X.basicOpen_le x
   · simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion]
-    -- Porting note: need an extra rewrite here, after simp, it is in `↔` form
-    rw [iff_iff_eq]
-    congr 3
+    congr! 1
     · refine congr_arg (Set.iUnion ·) ?_
       ext1 x
       exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _)
@@ -614,9 +612,7 @@ theorem of_affine_open_cover {X : Scheme} (V : X.affineOpens) (S : Set X.affineO
   have : ∀ (x : V.1), ∃ f : X.presheaf.obj <| op V.1,
       ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
     intro x
-    have : ↑x ∈ (Set.univ : Set X) := trivial
-    rw [← hS] at this
-    obtain ⟨W, hW⟩ := Set.mem_iUnion.mp this
+    obtain ⟨W, hW⟩ := Set.mem_iUnion.mp (by simpa only [← hS] using Set.mem_univ (x : X))
     obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop W.1.prop x ⟨x.prop, hW⟩
     refine' ⟨f, hf, _⟩
     convert hP₁ _ g (hS' W) using 1

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -54,10 +54,7 @@ variable {𝕜 E F : Type*} [RCLike 𝕜]
 variable [NormedAddCommGroup E] [NormedAddCommGroup F]
 variable [InnerProductSpace 𝕜 E] [InnerProductSpace ℝ F]
 
--- mathport name: «expr⟪ , ⟫»
 local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
-
--- mathport name: exprabsR
 local notation "absR" => abs
 
 /-! ### Orthogonal projection in inner product spaces -/

Mathlib/Analysis/Normed/Group/CocompactMap.lean

@@ -27,7 +27,7 @@ variable [NormedAddCommGroup E] [NormedAddCommGroup F] [ProperSpace E] [ProperSp
 variable {f : 𝓕}
 
 theorem CocompactMapClass.norm_le [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F] (ε : ℝ) :
-    ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ε < ‖f x‖ := by
+    ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖ := by
   have h := cocompact_tendsto f
   rw [tendsto_def] at h
   specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩)
@@ -39,7 +39,7 @@ theorem CocompactMapClass.norm_le [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F
   simp [hx]
 
 theorem Filter.tendsto_cocompact_cocompact_of_norm {f : E → F}
-    (h : ∀ ε : ℝ, ∃ r : ℝ, ∀ (x : E) (_hx : r < ‖x‖), ε < ‖f x‖) :
+    (h : ∀ ε : ℝ, ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) :
     Tendsto f (cocompact E) (cocompact F) := by
   rw [tendsto_def]
   intro s hs
@@ -53,6 +53,6 @@ theorem Filter.tendsto_cocompact_cocompact_of_norm {f : E → F}
   simp [hr x hx]
 
 theorem ContinuousMapClass.toCocompactMapClass_of_norm [FunLike 𝓕 E F] [ContinuousMapClass 𝓕 E F]
-    (h : ∀ (f : 𝓕) (ε : ℝ), ∃ r : ℝ, ∀ (x : E) (_hx : r < ‖x‖), ε < ‖f x‖) :
+    (h : ∀ (f : 𝓕) (ε : ℝ), ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) :
     CocompactMapClass 𝓕 E F where
   cocompact_tendsto := (tendsto_cocompact_cocompact_of_norm <| h ·)

Mathlib/CategoryTheory/Sites/Equivalence.lean

@@ -77,7 +77,7 @@ theorem coverPreserving : CoverPreserving J (e.locallyCoverDense J).inducedTopol
       simpa using S.downward_closed hg _
     · intro hf
       exact ⟨_, e.unitInv.app Z ≫ f ≫ e.unitInv.app U, S.downward_closed hf _,
-        e.unit.app Z ≫ e.unit.app _, (by simp)⟩
+        e.unit.app Z ≫ e.unit.app _, by simp⟩
 
 instance : IsCoverDense e.functor (e.locallyCoverDense J).inducedTopology where
   is_cover U := by
@@ -87,7 +87,7 @@ instance : IsCoverDense e.functor (e.locallyCoverDense J).inducedTopology where
     simp only [Sieve.functorPushforward_apply, Presieve.functorPushforward, exists_and_left,
       Sieve.top_apply, iff_true]
     exact ⟨e.functor.obj Y, (Adjunction.homEquiv e.toAdjunction _ _).symm f,
-      Presieve.in_coverByImage _ _, e.unit.app _, (by simp)⟩
+      Presieve.in_coverByImage _ _, e.unit.app _, by simp⟩
 
 instance : IsCoverDense e.inverse J where
   is_cover U := by

Mathlib/Data/Polynomial/Eval.lean

@@ -1094,8 +1094,8 @@ theorem eval₂_pow' (n : ℕ) :
 theorem eval₂_comp' : eval₂ (algebraMap R S) x (p.comp q) =
     eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p := by
   induction p using Polynomial.induction_on' with
-    | h_add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
-    | h_monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']
+  | h_add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
+  | h_monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']
 
 end Algebra
 

Mathlib/Data/Real/EReal.lean

@@ -450,10 +450,10 @@ theorem eq_bot_iff_forall_lt (x : EReal) : x = ⊥ ↔ ∀ y : ℝ, x < (y : ERe
 
 lemma exists_between_coe_real {x z : EReal} (h : x < z) : ∃ y : ℝ, x < y ∧ y < z := by
   obtain ⟨a, ha₁, ha₂⟩ := exists_between h
-  induction' a using EReal.rec with a₀
-  · exact (not_lt_bot ha₁).elim
-  · exact ⟨a₀, by exact_mod_cast ha₁, by exact_mod_cast ha₂⟩
-  · exact (not_top_lt ha₂).elim
+  induction a using EReal.rec with
+  | h_bot => exact (not_lt_bot ha₁).elim
+  | h_real a₀ => exact ⟨a₀, ha₁, ha₂⟩
+  | h_top => exact (not_top_lt ha₂).elim
 
 @[simp]
 lemma image_coe_Icc (x y : ℝ) : Real.toEReal '' Icc x y = Icc ↑x ↑y := by

Mathlib/Data/Set/Lattice.lean

@@ -31,7 +31,7 @@ for `Set α`, and some more set constructions.
   `f ⁻¹ y ⊆ s`.
 * `Set.seq`: Union of the image of a set under a **seq**uence of functions. `seq s t` is the union
   of `f '' t` over all `f ∈ s`, where `t : Set α` and `s : Set (α → β)`.
-* `Set.iUnion_eq_sigma_of_disjoint`: Equivalence between `⋃ i, t i` and `Σ i, t i`, where `t` is an
+* `Set.unionEqSigmaOfDisjoint`: Equivalence between `⋃ i, t i` and `Σ i, t i`, where `t` is an
   indexed family of disjoint sets.
 
 ## Naming convention

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -300,11 +300,12 @@ lemma minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ)
 lemma minpoly_algHom_toLinearMap (σ : L →ₐ[K] L) (hσ : IsOfFinOrder σ) :
     minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1 := by
   have : orderOf σ = orderOf (AlgEquiv.algHomUnitsEquiv _ _ hσ.unit) := by
-    erw [orderOf_injective (AlgEquiv.algHomUnitsEquiv K L)
-      (AlgEquiv.algHomUnitsEquiv K L).injective]
-    rw [← orderOf_units]
-    rfl
-  rw [this, ← minpoly_algEquiv_toLinearMap]; rfl
-  rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]
+    rw [← MonoidHom.coe_coe, orderOf_injective (AlgEquiv.algHomUnitsEquiv K L)
+      (AlgEquiv.algHomUnitsEquiv K L).injective, ← orderOf_units, IsOfFinOrder.val_unit]
+  rw [this, ← minpoly_algEquiv_toLinearMap]
+  · apply congr_arg
+    ext
+    simp
+  · rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]
 
 end AlgHom

Mathlib/FieldTheory/Perfect.lean

@@ -375,7 +375,8 @@ It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`. -/
 noncomputable def rootsExpandEquivRoots : (expand R p f).roots.toFinset ≃ f.roots.toFinset :=
   ((frobeniusEquiv R p).image _).trans <| .Set.ofEq <| show _ '' (setOf _) = setOf _ by
     classical simp_rw [← roots_expand_image_frobenius (p := p) (f := f), Finset.mem_val,
-      Finset.setOf_mem, Finset.coe_image]; rfl
+      Finset.setOf_mem, Finset.coe_image, RingEquiv.toEquiv_eq_coe, EquivLike.coe_coe,
+      frobeniusEquiv_apply]
 
 @[simp]
 theorem rootsExpandEquivRoots_apply (x) : (rootsExpandEquivRoots p f x : R) = x ^ p := rfl
@@ -387,7 +388,8 @@ noncomputable def rootsExpandPowEquivRoots (n : ℕ) :
     (expand R (p ^ n) f).roots.toFinset ≃ f.roots.toFinset :=
   ((iterateFrobeniusEquiv R p n).image _).trans <| .Set.ofEq <| show _ '' (setOf _) = setOf _ by
     classical simp_rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n),
-      Finset.mem_val, Finset.setOf_mem, Finset.coe_image]; rfl
+      Finset.mem_val, Finset.setOf_mem, Finset.coe_image, RingEquiv.toEquiv_eq_coe,
+      EquivLike.coe_coe, iterateFrobeniusEquiv_apply]
 
 @[simp]
 theorem rootsExpandPowEquivRoots_apply (n : ℕ) (x) :

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -271,14 +271,13 @@ theorem finite_tsupport : {i | x₀ ∈ tsupport (ρ i)}.Finite :=
 
 /-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
   This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/
-def fintsupport (x : M ): Finset ι :=
+def fintsupport (x : M) : Finset ι :=
   (ρ.finite_tsupport x).toFinset
 
 theorem mem_fintsupport_iff (i : ι) : i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport (ρ i) :=
   Finite.mem_toFinset _
 
-theorem eventually_fintsupport_subset :
-    ∀ᶠ y in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀ :=
+theorem eventually_fintsupport_subset : ∀ᶠ y in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀ :=
   ρ.toPartitionOfUnity.eventually_fintsupport_subset _
 
 theorem finsupport_subset_fintsupport : ρ.finsupport x₀ ⊆ ρ.fintsupport x₀ :=

Mathlib/GroupTheory/Perm/Cycle/Factors.lean

@@ -313,7 +313,7 @@ end CycleOf
 section cycleFactors
 
 open scoped List in
-/-- Given a list `l : List α` and a permutation `f : perm α` whose nonfixed points are all in `l`,
+/-- Given a list `l : List α` and a permutation `f : Perm α` whose nonfixed points are all in `l`,
   recursively factors `f` into cycles. -/
 def cycleFactorsAux [DecidableEq α] [Fintype α] :
     ∀ (l : List α) (f : Perm α),
@@ -352,8 +352,7 @@ def cycleFactorsAux [DecidableEq α] [Fintype α] :
               have hgm : (g::m.erase g) ~ m :=
                 List.cons_perm_iff_perm_erase.2 ⟨hg, List.Perm.refl _⟩
               have : ∀ h ∈ m.erase g, Disjoint g h :=
-                (List.pairwise_cons.1
-                    ((hgm.pairwise_iff @fun a b (h : Disjoint a b) => h.symm).2 hm₃)).1
+                (List.pairwise_cons.1 ((hgm.pairwise_iff Disjoint.symm).2 hm₃)).1
               by_cases id fun hgy : g y ≠ y =>
                 (disjoint_prod_right _ this y).resolve_right <| by
                   have hsc : SameCycle f⁻¹ x (f y) := by

Mathlib/LinearAlgebra/Dual.lean

@@ -662,7 +662,7 @@ def evalEquiv : M ≃ₗ[R] Dual R (Dual R M) :=
 
 /-- The dual of a reflexive module is reflexive. -/
 instance Dual.instIsReflecive : IsReflexive R (Dual R M) :=
-⟨by simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective⟩
+  ⟨by simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective⟩
 
 /-- The isomorphism `Module.evalEquiv` induces an order isomorphism on subspaces. -/
 def mapEvalEquiv : Submodule R M ≃o Submodule R (Dual R (Dual R M)) :=

Mathlib/LinearAlgebra/Matrix/ToLin.lean

@@ -655,8 +655,8 @@ theorem LinearMap.toMatrix_reindexRange [DecidableEq M₁] [DecidableEq M₂] (f
     (i : n) :
     LinearMap.toMatrix v₁.reindexRange v₂.reindexRange f ⟨v₂ k, Set.mem_range_self k⟩
         ⟨v₁ i, Set.mem_range_self i⟩ =
-      LinearMap.toMatrix v₁ v₂ f k i :=
-  by simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
+      LinearMap.toMatrix v₁ v₂ f k i := by
+  simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
 #align linear_map.to_matrix_reindex_range LinearMap.toMatrix_reindexRange
 
 variable {M₃ : Type*} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃)
@@ -812,14 +812,14 @@ theorem Matrix.toLinAlgEquiv_one : Matrix.toLinAlgEquiv v₁ 1 = LinearMap.id :=
 theorem LinearMap.toMatrixAlgEquiv_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
     LinearMap.toMatrixAlgEquiv v₁.reindexRange f
         ⟨v₁ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ =
-      LinearMap.toMatrixAlgEquiv v₁ f k i :=
-  by simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
+      LinearMap.toMatrixAlgEquiv v₁ f k i := by
+  simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
 #align linear_map.to_matrix_alg_equiv_reindex_range LinearMap.toMatrixAlgEquiv_reindexRange
 
 theorem LinearMap.toMatrixAlgEquiv_comp (f g : M₁ →ₗ[R] M₁) :
     LinearMap.toMatrixAlgEquiv v₁ (f.comp g) =
-      LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g :=
-  by simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]
+      LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g := by
+  simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]
 #align linear_map.to_matrix_alg_equiv_comp LinearMap.toMatrixAlgEquiv_comp
 
 theorem LinearMap.toMatrixAlgEquiv_mul (f g : M₁ →ₗ[R] M₁) :
@@ -830,15 +830,15 @@ theorem LinearMap.toMatrixAlgEquiv_mul (f g : M₁ →ₗ[R] M₁) :
 
 theorem Matrix.toLinAlgEquiv_mul (A B : Matrix n n R) :
     Matrix.toLinAlgEquiv v₁ (A * B) =
-      (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B) :=
-  by convert Matrix.toLin_mul v₁ v₁ v₁ A B
+      (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B) := by
+  convert Matrix.toLin_mul v₁ v₁ v₁ A B
 #align matrix.to_lin_alg_equiv_mul Matrix.toLinAlgEquiv_mul
 
 @[simp]
 theorem Matrix.toLin_finTwoProd_apply (a b c d : R) (x : R × R) :
     Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R) !![a, b; c, d] x =
-      (a * x.fst + b * x.snd, c * x.fst + d * x.snd) :=
-  by simp [Matrix.toLin_apply, Matrix.mulVec, Matrix.dotProduct]
+      (a * x.fst + b * x.snd, c * x.fst + d * x.snd) := by
+  simp [Matrix.toLin_apply, Matrix.mulVec, Matrix.dotProduct]
 #align matrix.to_lin_fin_two_prod_apply Matrix.toLin_finTwoProd_apply
 
 theorem Matrix.toLin_finTwoProd (a b c d : R) :

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -334,13 +334,13 @@ protected theorem add_smul (r s : R'') (x : M ⊗[R] N) : (r + s) • x = r •
 #align tensor_product.add_smul TensorProduct.add_smul
 
 instance addMonoid : AddMonoid (M ⊗[R] N) :=
-{ TensorProduct.addZeroClass _ _ with
-  toAddSemigroup := TensorProduct.addSemigroup _ _
-  toZero := (TensorProduct.addZeroClass _ _).toZero
-  nsmul := fun n v => n • v
-  nsmul_zero := by simp [TensorProduct.zero_smul]
-  nsmul_succ := by simp only [TensorProduct.one_smul, TensorProduct.add_smul, add_comm,
-    forall_const] }
+  { TensorProduct.addZeroClass _ _ with
+    toAddSemigroup := TensorProduct.addSemigroup _ _
+    toZero := (TensorProduct.addZeroClass _ _).toZero
+    nsmul := fun n v => n • v
+    nsmul_zero := by simp [TensorProduct.zero_smul]
+    nsmul_succ := by simp only [TensorProduct.one_smul, TensorProduct.add_smul, add_comm,
+      forall_const] }
 
 instance addCommMonoid : AddCommMonoid (M ⊗[R] N) :=
   { TensorProduct.addCommSemigroup _ _ with

Mathlib/Logic/Function/Basic.lean

@@ -806,7 +806,7 @@ namespace FactorsThrough
 
 protected theorem rfl {f : α → β} : FactorsThrough f f := fun _ _ ↦ id
 
-theorem comp_left {f : α → β} {g : α → γ}  (h : FactorsThrough g f) (g' : γ → δ) :
+theorem comp_left {f : α → β} {g : α → γ} (h : FactorsThrough g f) (g' : γ → δ) :
     FactorsThrough (g' ∘ g) f := fun _x _y hxy ↦
   congr_arg g' (h hxy)
 

Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

@@ -131,7 +131,7 @@ theorem set_integral_abs_condexp_le {s : Set α} (hs : MeasurableSet[m] s) (f :
       (condexp_indicator hfint hs).fun_comp abs
     refine' EventuallyEq.trans (eventually_of_forall fun x => _) this.symm
     rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
-    rfl
+    simp only [Real.norm_eq_abs]
   rw [this, ← integral_indicator (hnm _ hs)]
   refine' (integral_abs_condexp_le _).trans
     (le_of_eq <| integral_congr_ae <| eventually_of_forall fun x => _)
@@ -229,7 +229,8 @@ theorem condexp_stronglyMeasurable_simpleFunc_mul (hm : m ≤ m0) (f : @SimpleFu
     intro s c f
     ext1 x
     by_cases hx : x ∈ s
-    · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul]; rfl
+    · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul,
+        Function.const_apply]
     · simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, zero_mul]
   apply @SimpleFunc.induction _ _ m _ (fun f => _)
     (fun c s hs => ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ => ?_) f