chore: tidy various files (#8823)

Counterexamples/Phillips.lean

@@ -570,9 +570,9 @@ theorem countable_ne (Hcont : #ℝ = aleph 1) (φ : (DiscreteCopy ℝ →ᵇ ℝ
     {x | φ.toBoundedAdditiveMeasure.continuousPart univ ≠ φ (f Hcont x)} ⊆
       {x | φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x ≠ ∅} := by
     intro x hx
+    simp only [mem_setOf] at *
     contrapose! hx
-    simp only [Classical.not_not, mem_setOf_eq, not_nonempty_iff_eq_empty] at hx
-    simp [apply_f_eq_continuousPart Hcont φ x hx]
+    exact apply_f_eq_continuousPart Hcont φ x hx |>.symm
   have B :
     {x | φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x ≠ ∅} ⊆
       ⋃ y ∈ φ.toBoundedAdditiveMeasure.discreteSupport, {x | y ∈ spf Hcont x} := by

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -233,13 +233,13 @@ theorem hom_apply {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K
 @[simp]
 theorem whiskerLeft_apply (L : ModuleCat.{u} R) {M N : ModuleCat.{u} R} (f : M ⟶ N)
     (l : L) (m : M) :
-      (L ◁ f) (l ⊗ₜ m) = l ⊗ₜ f m :=
+    (L ◁ f) (l ⊗ₜ m) = l ⊗ₜ f m :=
   rfl
 
 @[simp]
 theorem whiskerRight_apply {L M : ModuleCat.{u} R} (f : L ⟶ M) (N : ModuleCat.{u} R)
     (l : L) (n : N) :
-      (f ▷ N) (l ⊗ₜ n) = f l ⊗ₜ n :=
+    (f ▷ N) (l ⊗ₜ n) = f l ⊗ₜ n :=
   rfl
 
 @[simp]

Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean

@@ -140,15 +140,15 @@ section
 variable [S₁.HasLeftHomology] [S₂.HasLeftHomology]
 
 @[simp]
-lemma leftHomologyMap_neg : leftHomologyMap (-φ)  = -leftHomologyMap φ :=
+lemma leftHomologyMap_neg : leftHomologyMap (-φ) = -leftHomologyMap φ :=
   leftHomologyMap'_neg _ _
 
 @[simp]
 lemma cyclesMap_neg : cyclesMap (-φ) = -cyclesMap φ :=
   cyclesMap'_neg _ _
 
 @[simp]
-lemma leftHomologyMap_add : leftHomologyMap (φ + φ')  = leftHomologyMap φ + leftHomologyMap φ' :=
+lemma leftHomologyMap_add : leftHomologyMap (φ + φ') = leftHomologyMap φ + leftHomologyMap φ' :=
   leftHomologyMap'_add _ _
 
 @[simp]
@@ -249,7 +249,7 @@ section
 variable [S₁.HasRightHomology] [S₂.HasRightHomology]
 
 @[simp]
-lemma rightHomologyMap_neg : rightHomologyMap (-φ)  = -rightHomologyMap φ :=
+lemma rightHomologyMap_neg : rightHomologyMap (-φ) = -rightHomologyMap φ :=
   rightHomologyMap'_neg _ _
 
 @[simp]
@@ -258,7 +258,7 @@ lemma opcyclesMap_neg : opcyclesMap (-φ) = -opcyclesMap φ :=
 
 @[simp]
 lemma rightHomologyMap_add :
-    rightHomologyMap (φ + φ')  = rightHomologyMap φ + rightHomologyMap φ' :=
+    rightHomologyMap (φ + φ') = rightHomologyMap φ + rightHomologyMap φ' :=
   rightHomologyMap'_add _ _
 
 @[simp]
@@ -332,11 +332,11 @@ section
 variable [S₁.HasHomology] [S₂.HasHomology]
 
 @[simp]
-lemma homologyMap_neg : homologyMap (-φ)  = -homologyMap φ :=
+lemma homologyMap_neg : homologyMap (-φ) = -homologyMap φ :=
   homologyMap'_neg _ _
 
 @[simp]
-lemma homologyMap_add : homologyMap (φ + φ')  = homologyMap φ + homologyMap φ' :=
+lemma homologyMap_add : homologyMap (φ + φ') = homologyMap φ + homologyMap φ' :=
   homologyMap'_add _ _
 
 @[simp]

Mathlib/Algebra/Lie/Killing.lean

@@ -190,7 +190,9 @@ lemma eq_zero_of_mem_weightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L]
     B m₀ m₁ = 0 := by
   replace hB : ∀ x (k : ℕ) m n, B m ((φ x ^ k) n) = (- 1 : R) ^ k • B ((φ x ^ k) m) n := by
     intro x k
-    induction' k with k ih; simp
+    induction k with
+    | zero => simp
+    | succ k ih =>
     intro m n
     replace hB : ∀ m, B m (φ x n) = (- 1 : R) • B (φ x m) n := by simp [hB]
     have : (-1 : R) ^ k • (-1 : R) = (-1 : R) ^ (k + 1) := by rw [pow_succ' (-1 : R), smul_eq_mul]

Mathlib/Algebra/Module/Zlattice.lean

@@ -320,7 +320,8 @@ theorem measure_fundamentalDomain_ne_zero [Finite ι] [MeasurableSpace E] [Borel
     {μ : Measure E} [Measure.IsAddHaarMeasure μ] :
     μ (fundamentalDomain b) ≠ 0 := by
   convert (Zspan.isAddFundamentalDomain b μ).measure_ne_zero (NeZero.ne μ)
-  exact (by infer_instance : Countable (span ℤ (Set.range b)))
+  simp only [mem_toAddSubgroup]
+  infer_instance
 
 theorem measure_fundamentalDomain [Fintype ι] [DecidableEq ι] [MeasurableSpace E] (μ : Measure E)
     [BorelSpace E] [Measure.IsAddHaarMeasure μ] (b₀ : Basis ι ℝ E) :

Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

@@ -29,7 +29,7 @@ We also provide estimates in the case if `g x` is close to `g x₀` on this ball
   If `(φ i).rOut` tends to zero along a filter `l`,
   then `((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀` tends to `g x₀` along the same filter.
 - `ContDiffBump.convolution_tendsto_right`: generalization of the above lemma.
-- `ContDiffBump.ae_convolution_tendsto_right_of_locally_integrable`: let `g` be a locally
+- `ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable`: let `g` be a locally
   integrable function. Then the convolution of `g` with a family of bump functions with
   support tending to `0` converges almost everywhere to `g`.
 
@@ -108,7 +108,7 @@ theorem convolution_tendsto_right_of_continuous {ι} {φ : ι → ContDiffBump (
 /-- If a function `g` is locally integrable, then the convolution `φ i * g` converges almost
 everywhere to `g` if `φ i` is a sequence of bump functions with support tending to `0`, provided
 that the ratio between the inner and outer radii of `φ i` remains bounded. -/
-theorem ae_convolution_tendsto_right_of_locally_integrable
+theorem ae_convolution_tendsto_right_of_locallyIntegrable
     {ι} {φ : ι → ContDiffBump (0 : G)} {l : Filter ι} {K : ℝ}
     (hφ : Tendsto (fun i ↦ (φ i).rOut) l (𝓝 0))
     (h'φ : ∀ᶠ i in l, (φ i).rOut ≤ K * (φ i).rIn) (hg : LocallyIntegrable g μ) : ∀ᵐ x₀ ∂μ,

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -367,11 +367,11 @@ def fpowerSeries (f : E →L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 E F
   | _ => 0
 #align continuous_linear_map.fpower_series ContinuousLinearMap.fpowerSeries
 
-theorem fpower_series_apply_zero (f : E →L[𝕜] F) (x : E) :
+theorem fpowerSeries_apply_zero (f : E →L[𝕜] F) (x : E) :
     f.fpowerSeries x 0 = ContinuousMultilinearMap.curry0 𝕜 _ (f x) :=
   rfl
 
-theorem fpower_series_apply_one (f : E →L[𝕜] F) (x : E) :
+theorem fpowerSeries_apply_one (f : E →L[𝕜] F) (x : E) :
     f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f :=
   rfl
 
@@ -380,7 +380,7 @@ theorem fpowerSeries_apply_add_two (f : E →L[𝕜] F) (x : E) (n : ℕ) : f.fp
 #align continuous_linear_map.fpower_series_apply_add_two ContinuousLinearMap.fpowerSeries_apply_add_two
 
 attribute
-  [eqns fpower_series_apply_zero fpower_series_apply_one fpowerSeries_apply_add_two] fpowerSeries
+  [eqns fpowerSeries_apply_zero fpowerSeries_apply_one fpowerSeries_apply_add_two] fpowerSeries
 attribute [simp] fpowerSeries
 
 end ContinuousLinearMap

Mathlib/CategoryTheory/Monoidal/Transport.lean

@@ -17,7 +17,7 @@ we can transport a monoidal structure on `C` along the equivalence as
 More generally, we can transport the lawfulness of a monoidal structure along a suitable faithful
 functor, as `CategoryTheory.Monoidal.induced`.
 The comparison is analogous to the difference between `Equiv.monoid` and
-`Function.Injective.Monoid`.
+`Function.Injective.monoid`.
 
 We then upgrade the original functor and its inverse to monoidal functors
 with respect to the new monoidal structure on `D`.

Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

@@ -12,7 +12,7 @@ import Mathlib.Tactic.ApplyFun
 /-!
 # The equalizer diagram sheaf condition for a presieve
 
-In `Mathlib/CategoryTheory/Sites/IsSheafFor` it is defined what it means for a presheaf to be a
+In `Mathlib/CategoryTheory/Sites/IsSheafFor.lean` it is defined what it means for a presheaf to be a
 sheaf *for* a particular presieve. In this file we provide equivalent conditions in terms of
 equalizer diagrams.
 

Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

@@ -15,7 +15,7 @@ Defines the notion of a sheaf of types (usually called a sheaf of sets by mathem
 on a category equipped with a Grothendieck topology, as well as a range of equivalent
 conditions useful in different situations.
 
-In `Mathlib/CategoryTheory/Sites/IsSheafFor` it is defined what it means for a presheaf to be a
+In `Mathlib/CategoryTheory/Sites/IsSheafFor.lean` it is defined what it means for a presheaf to be a
 sheaf *for* a particular sieve. Given a Grothendieck topology `J`, `P` is a sheaf if it is a sheaf
 for every sieve in the topology. See `IsSheaf`.
 

Mathlib/Data/List/Basic.lean

@@ -4474,7 +4474,7 @@ section Disjoint
 
 variable {α β : Type*}
 
-/-- The images of disjoint maps under a map are disjoint -/
+/-- The images of disjoint lists under an injective map are disjoint -/
 theorem disjoint_map {f : α → β} {s t : List α} (hf : Function.Injective f)
     (h : Disjoint s t) : Disjoint (s.map f) (t.map f) := by
   simp only [Disjoint]

Mathlib/Data/List/Range.lean

@@ -243,7 +243,7 @@ section Ranges
 * Example: `[1,2,3].ranges = [[0],[1,2],[3,4,5]]` -/
 def ranges : List ℕ → List (List ℕ)
   | [] => nil
-  | a::l => range a::(ranges l).map (map (Nat.add a))
+  | a::l => range a::(ranges l).map (map (a + ·))
 
 /-- The members of `l.ranges` are pairwise disjoint -/
 theorem ranges_disjoint (l : List ℕ) :
@@ -287,7 +287,6 @@ theorem ranges_join (l : List ℕ) :
     simp only [sum_cons, join]
     rw [← map_join, hl]
     rw [range_add]
-    rfl
 
 /-- Any entry of any member of `l.ranges` is strictly smaller than `l.sum` -/
 theorem mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :

Mathlib/Data/Nat/Cast/Defs.lean

@@ -63,8 +63,8 @@ instance instOfNat [NatCast R] [Nat.AtLeastTwo n] : OfNat R n where
 
 library_note "no_index around OfNat.ofNat"
 /--
-When writing lemmas about `OfNat.ofNat` that assume `Nat.AtLeastTwo`, the term need to be wrapped in
-`no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.
+When writing lemmas about `OfNat.ofNat` that assume `Nat.AtLeastTwo`, the term needs to be wrapped
+in `no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.
 
 Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).
 -/

Mathlib/Data/Num/Lemmas.lean

@@ -86,8 +86,8 @@ theorem add_one (n : PosNum) : n + 1 = succ n := by cases n <;> rfl
 
 @[norm_cast]
 theorem add_to_nat : ∀ m n, ((m + n : PosNum) : ℕ) = m + n
-  | 1, b => by rw [one_add b, succ_to_nat, add_comm]; rfl
-  | a, 1 => by rw [add_one a, succ_to_nat]; rfl
+  | 1, b => by rw [one_add b, succ_to_nat, add_comm, cast_one]
+  | a, 1 => by rw [add_one a, succ_to_nat, cast_one]
   | bit0 a, bit0 b => (congr_arg _root_.bit0 (add_to_nat a b)).trans <| add_add_add_comm _ _ _ _
   | bit0 a, bit1 b =>
     (congr_arg _root_.bit1 (add_to_nat a b)).trans <|
@@ -113,11 +113,11 @@ theorem add_succ : ∀ m n : PosNum, m + succ n = succ (m + n)
 theorem bit0_of_bit0 : ∀ n, _root_.bit0 n = bit0 n
   | 1 => rfl
   | bit0 p => congr_arg bit0 (bit0_of_bit0 p)
-  | bit1 p => show bit0 (succ (_root_.bit0 p)) = _ by rw [bit0_of_bit0 p]; rfl
+  | bit1 p => show bit0 (succ (_root_.bit0 p)) = _ by rw [bit0_of_bit0 p, succ]
 #align pos_num.bit0_of_bit0 PosNum.bit0_of_bit0
 
 theorem bit1_of_bit1 (n : PosNum) : _root_.bit1 n = bit1 n :=
-  show _root_.bit0 n + 1 = bit1 n by rw [add_one, bit0_of_bit0]; rfl
+  show _root_.bit0 n + 1 = bit1 n by rw [add_one, bit0_of_bit0, succ]
 #align pos_num.bit1_of_bit1 PosNum.bit1_of_bit1
 
 @[norm_cast]
@@ -218,7 +218,7 @@ theorem add_one : ∀ n : Num, n + 1 = succ n
 
 theorem add_succ : ∀ m n : Num, m + succ n = succ (m + n)
   | 0, n => by simp [zero_add]
-  | pos p, 0 => show pos (p + 1) = succ (pos p + 0) by rw [PosNum.add_one, add_zero]; rfl
+  | pos p, 0 => show pos (p + 1) = succ (pos p + 0) by rw [PosNum.add_one, add_zero, succ, succ']
   | pos p, pos q => congr_arg pos (PosNum.add_succ _ _)
 #align num.add_succ Num.add_succ
 
@@ -250,7 +250,7 @@ theorem bit1_succ : ∀ n : Num, n.bit1.succ = n.succ.bit0
 #align num.bit1_succ Num.bit1_succ
 
 theorem ofNat'_succ : ∀ {n}, ofNat' (n + 1) = ofNat' n + 1 :=
-  @(Nat.binaryRec (by simp; rfl) fun b n ih => by
+  @(Nat.binaryRec (by simp [zero_add]) fun b n ih => by
     cases b
     · erw [ofNat'_bit true n, ofNat'_bit]
       simp only [← bit1_of_bit1, ← bit0_of_bit0, cond, _root_.bit1]

Mathlib/Data/Polynomial/FieldDivision.lean

@@ -486,7 +486,7 @@ theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p := by
   classical
   have : Prime (normalize p) :=
     Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
-      (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp only [degree_zero]; decide))
+      (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp [degree_zero, ← WithBot.coe_one]))
   exact (normalize_associated _).prime this
 #align polynomial.prime_of_degree_eq_one Polynomial.prime_of_degree_eq_one
 

Mathlib/Data/Polynomial/RingDivision.lean

@@ -1338,7 +1338,7 @@ theorem map_roots_le [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p
 theorem map_roots_le_of_injective [IsDomain A] [IsDomain B] (p : A[X]) {f : A →+* B}
     (hf : Function.Injective f) : p.roots.map f ≤ (p.map f).roots := by
   by_cases hp0 : p = 0
-  · simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_zero]; rfl
+  · simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_zero, le_rfl]
   exact map_roots_le ((Polynomial.map_ne_zero_iff hf).mpr hp0)
 #align polynomial.map_roots_le_of_injective Polynomial.map_roots_le_of_injective
 
@@ -1351,7 +1351,7 @@ theorem card_roots_le_map [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (
 theorem card_roots_le_map_of_injective [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B}
     (hf : Function.Injective f) : Multiset.card p.roots ≤ Multiset.card (p.map f).roots := by
   by_cases hp0 : p = 0
-  · simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero]; rfl
+  · simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero, le_rfl]
   exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)
 #align polynomial.card_roots_le_map_of_injective Polynomial.card_roots_le_map_of_injective
 

Mathlib/Data/Polynomial/UnitTrinomial.lean

@@ -202,7 +202,7 @@ theorem isUnitTrinomial_iff' :
       sum_insert (mt mem_insert.mp (not_or_of_not hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
       sum_insert (mt mem_singleton.mp hmn.ne), sum_singleton, trinomial_leading_coeff' hkm hmn,
       trinomial_middle_coeff hkm hmn, trinomial_trailing_coeff' hkm hmn]
-    simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq]
+    simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq, Units.val_one]
     decide
   · have key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1 := fun k hk =>
       Int.sq_eq_one_of_sq_le_three

Mathlib/Data/Rat/Lemmas.lean

@@ -232,8 +232,7 @@ theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprim
 theorem coe_int_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n := by
   by_cases hn : n = 0
   · subst hn
-    simp only [Int.cast_zero, Int.zero_div, zero_div]
-    rfl
+    simp only [Int.cast_zero, Int.zero_div, zero_div, Int.ediv_zero]
   · have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn
     simp only [Int.ediv_self hn, Int.cast_one, Ne.def, not_false_iff, div_self this]
 #align rat.coe_int_div_self Rat.coe_int_div_self

Mathlib/Data/Real/ENNReal.lean

@@ -640,7 +640,7 @@ theorem mul_lt_top_iff {a b : ℝ≥0∞} : a * b < ∞ ↔ a < ∞ ∧ b < ∞
 theorem mul_self_lt_top_iff {a : ℝ≥0∞} : a * a < ⊤ ↔ a < ⊤ := by
   rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]
   rintro rfl
-  decide
+  exact zero_lt_top
 #align ennreal.mul_self_lt_top_iff ENNReal.mul_self_lt_top_iff
 
 theorem mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b :=
@@ -1801,7 +1801,7 @@ theorem add_thirds (a : ℝ≥0∞) : a / 3 + a / 3 + a / 3 = a := by
 #align ennreal.div_pos_iff ENNReal.div_pos_iff
 
 protected theorem half_pos (h : a ≠ 0) : 0 < a / 2 := by
-  simp only [div_pos_iff, ne_eq, h, not_false_eq_true]; decide
+  simp only [div_pos_iff, ne_eq, h, not_false_eq_true, two_ne_top, and_self]
 #align ennreal.half_pos ENNReal.half_pos
 
 protected theorem one_half_lt_one : (2⁻¹ : ℝ≥0∞) < 1 :=

Mathlib/Data/Sign.lean

@@ -34,7 +34,7 @@ namespace SignType
 
 -- Porting note: Added Fintype SignType manually
 instance : Fintype SignType :=
-   Fintype.ofMultiset (zero :: neg :: pos :: List.nil) (fun x ↦ by cases x <;> decide)
+   Fintype.ofMultiset (zero :: neg :: pos :: List.nil) (fun x ↦ by cases x <;> simp)
 
 instance : Zero SignType :=
   ⟨zero⟩

Mathlib/GroupTheory/Subgroup/Finite.lean

@@ -174,7 +174,7 @@ theorem card_le_one_iff_eq_bot [Fintype H] : Fintype.card H ≤ 1 ↔ H = ⊥ :=
 #align add_subgroup.card_nonpos_iff_eq_bot AddSubgroup.card_le_one_iff_eq_bot
 
 @[to_additive] lemma eq_bot_iff_card [Fintype H] : H = ⊥ ↔ Fintype.card H = 1 :=
-  ⟨by rintro rfl;  exact card_bot, eq_bot_of_card_eq _⟩
+  ⟨by rintro rfl; exact card_bot, eq_bot_of_card_eq _⟩
 
 @[to_additive one_lt_card_iff_ne_bot]
 theorem one_lt_card_iff_ne_bot [Fintype H] : 1 < Fintype.card H ↔ H ≠ ⊥ :=

Mathlib/GroupTheory/Submonoid/Operations.lean

@@ -1376,8 +1376,7 @@ theorem eq_bot_iff_forall : S = ⊥ ↔ ∀ x ∈ S, x = (1 : M) :=
 theorem eq_bot_of_subsingleton [Subsingleton S] : S = ⊥ := by
   rw [eq_bot_iff_forall]
   intro y hy
-  change ((⟨y, hy⟩ : S) : M) = (1 : S)
-  rw [Subsingleton.elim (⟨y, hy⟩ : S) 1]
+  simpa using _root_.congr_arg ((↑) : S → M) <| Subsingleton.elim (⟨y, hy⟩ : S) 1
 
 @[to_additive]
 theorem nontrivial_iff_exists_ne_one (S : Submonoid M) : Nontrivial S ↔ ∃ x ∈ S, x ≠ (1 : M) :=

Mathlib/MeasureTheory/Constructions/Prod/Integral.lean

@@ -514,7 +514,7 @@ theorem set_integral_prod (f : α × β → E) {s : Set α} {t : Set β}
 
 theorem integral_prod_smul {𝕜 : Type*} [IsROrC 𝕜] [NormedSpace 𝕜 E] (f : α → 𝕜) (g : β → E) :
     ∫ z, f z.1 • g z.2 ∂μ.prod ν = (∫ x, f x ∂μ) • ∫ y, g y ∂ν := by
-  by_cases hE : CompleteSpace E; swap; simp [integral, hE]
+  by_cases hE : CompleteSpace E; swap; · simp [integral, hE]
   by_cases h : Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν)
   · rw [integral_prod _ h]
     simp_rw [integral_smul, integral_smul_const]

Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

@@ -65,7 +65,7 @@ theorem exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure [NormedAddC
     [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [IsAddHaarMeasure μ]
     {L : AddSubgroup E} [Countable L] (fund : IsAddFundamentalDomain L F μ)
     (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h : μ F * 2 ^ finrank ℝ E < μ s) :
-    ∃ (x : _) (_ : x ≠ 0), ((x : L) : E) ∈ s := by
+    ∃ x ≠ 0, ((x : L) : E) ∈ s := by
   have h_vol : μ F < μ ((2⁻¹ : ℝ) • s) := by
     rw [addHaar_smul_of_nonneg μ (by norm_num : 0 ≤ (2 : ℝ)⁻¹) s, ←
       mul_lt_mul_right (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (pow_ne_top two_ne_top),
@@ -94,12 +94,12 @@ theorem exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure [NormedAddC
     {L : AddSubgroup E} [Countable L] [DiscreteTopology L] (fund : IsAddFundamentalDomain L F μ)
     (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h_cpt : IsCompact s)
     (h : μ F * 2 ^ finrank ℝ E ≤ μ s) :
-    ∃ (x : _) (_ : x ≠ 0), ((x : L) : E) ∈ s := by
+    ∃ x ≠ 0, ((x : L) : E) ∈ s := by
   have h_mes : μ s ≠ 0 := by
-    by_contra hμ
-    suffices μ F = 0 by exact fund.measure_ne_zero (NeZero.ne μ) this
+    intro hμ
+    suffices μ F = 0 from fund.measure_ne_zero (NeZero.ne μ) this
     rw [hμ, le_zero_iff, mul_eq_zero] at h
-    exact h.resolve_right <| (pow_eq_zero_iff finrank_pos).not.mpr two_ne_zero
+    exact h.resolve_right <| (pow_ne_zero_iff finrank_pos).mpr two_ne_zero
   have h_nemp : s.Nonempty := nonempty_of_measure_ne_zero h_mes
   let u : ℕ → ℝ≥0 := (exists_seq_strictAnti_tendsto 0).choose
   let K : ConvexBody E := ⟨s, h_conv, h_cpt, h_nemp⟩

Mathlib/MeasureTheory/Integral/SetIntegral.lean

@@ -1179,8 +1179,8 @@ theorem integral_comp_comm' (L : E →L[𝕜] F) {K} (hL : AntilipschitzWith K L
   by_cases h : Integrable φ μ
   · exact integral_comp_comm L h
   have : ¬Integrable (fun a => L (φ a)) μ := by
-    erw [LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]
-    assumption
+    rwa [← Function.comp_def,
+      LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]
   simp [integral_undef, h, this]
 #align continuous_linear_map.integral_comp_comm' ContinuousLinearMap.integral_comp_comm'