chore: tidy various files (#21568)

Archive/Imo/Imo1982Q1.lean

@@ -64,11 +64,9 @@ lemma f₁ : f 1 = 0 := by
   · cases Nat.succ_ne_zero _ h₂.symm
 
 lemma f₃ : f 3 = 1 := by
-    have h : f 3 = f 2 + f 1 ∨ f 3  = f 2 + f 1 + 1 := by apply hf.rel 2 1
-    rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
-    have not_left : ¬ f 3 = 0 := by apply ne_of_gt hf.hf₃
-    rw [or_iff_right (not_left)] at h
-    exact h
+  have h : f 3 = f 2 + f 1 ∨ f 3 = f 2 + f 1 + 1 := hf.rel 2 1
+  rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
+  exact h.resolve_left hf.hf₃.ne'
 
 lemma superadditive {m n : ℕ+} : f m + f n ≤ f (m + n) := by
   have h := hf.rel m n
@@ -98,7 +96,7 @@ lemma part_1 : 660 ≤ f (1980) := by
 
 lemma part_2 : f 1980 ≤ 660 := by
   have h : 5 * f 1980 + 33 * f 3 ≤ 5 * 660 + 33 := by
-    calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤  f (5 * 1980 + 33 * 3) := by apply hf.superlinear
+    calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤ f (5 * 1980 + 33 * 3) := by apply hf.superlinear
     _ = f 9999 := by rfl
     _ = 5 * 660 + 33 := by rw [hf.f_9999]
   rw [hf.f₃, mul_one] at h

Mathlib/Algebra/Algebra/Operations.lean

@@ -355,11 +355,11 @@ theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap
     LinearMap.toSpanSingleton_eq_algebra_linearMap]
 
 theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) := by
-  rw [one_eq_range]; exact LinearMap.mem_range_self _ _
+  simp [one_eq_range]
 
 @[simp]
 theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x := by
-  rw [one_eq_range]; rfl
+  simp [one_eq_range]
 
 protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
     map f.toLinearMap (1 : Submodule R A) = 1 := by

Mathlib/Algebra/BrauerGroup/Defs.lean

@@ -14,7 +14,7 @@ import Mathlib.Algebra.Category.AlgebraCat.Basic
 We introduce the definition of Brauer group of a field K, which is the quotient of the set of
 all finite-dimensional central simple algebras over K modulo the Brauer Equivalence where two
 central simple algebras `A` and `B` are Brauer Equivalent if there exist `n, m ∈ ℕ+` such
-that `Mₙ(A) ≃ₐ[K] Mₙ(B)`.
+that `Mₙ(A) ≃ₐ[K] Mₘ(B)`.
 
 # TODOs
 1. Prove that the Brauer group is an abelian group where multiplication is defined as tensorproduct.
@@ -49,18 +49,18 @@ attribute [instance] CSA.isCentral CSA.isSimple CSA.fin_dim
 /-- Two finite dimensional central simple algebras `A` and `B` are Brauer Equivalent
   if there exist `n, m ∈ ℕ+` such that the `Mₙ(A) ≃ₐ[K] Mₙ(B)`. -/
 abbrev IsBrauerEquivalent (A B : CSA K) : Prop :=
-  ∃n m : ℕ, n ≠ 0 ∧ m ≠ 0 ∧ (Nonempty <| Matrix (Fin n) (Fin n) A ≃ₐ[K] Matrix (Fin m) (Fin m) B)
+  ∃ n m : ℕ, n ≠ 0 ∧ m ≠ 0 ∧ (Nonempty <| Matrix (Fin n) (Fin n) A ≃ₐ[K] Matrix (Fin m) (Fin m) B)
 
 namespace IsBrauerEquivalent
 
 @[refl]
 lemma refl (A : CSA K) : IsBrauerEquivalent A A :=
-    ⟨1, 1, one_ne_zero, one_ne_zero, ⟨AlgEquiv.refl⟩⟩
+  ⟨1, 1, one_ne_zero, one_ne_zero, ⟨AlgEquiv.refl⟩⟩
 
 @[symm]
 lemma symm {A B : CSA K} (h : IsBrauerEquivalent A B) : IsBrauerEquivalent B A :=
-    let ⟨n, m, hn, hm, ⟨iso⟩⟩ := h
-    ⟨m, n, hm, hn, ⟨iso.symm⟩⟩
+  let ⟨n, m, hn, hm, ⟨iso⟩⟩ := h
+  ⟨m, n, hm, hn, ⟨iso.symm⟩⟩
 
 open Matrix in
 @[trans]

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -412,8 +412,10 @@ theorem distribMulActionHom_ext' {N : Type*} [Monoid R] [Semiring k] [AddMonoid
 abbrev lsingle [Semiring R] [Semiring k] [Module R k] (a : G) :
     k →ₗ[R] MonoidAlgebra k G := Finsupp.lsingle a
 
-@[simp] lemma lsingle_apply [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
-  lsingle (R := R) a b = single a b := rfl
+@[simp]
+lemma lsingle_apply [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
+    lsingle (R := R) a b = single a b :=
+  rfl
 
 /-- A copy of `Finsupp.lhom_ext'` for `MonoidAlgebra`. -/
 @[ext high]

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -638,9 +638,8 @@ section CommSemiring
 
 variable [CommSemiring R] {a p : R[X]}
 
-theorem eq_zero_of_mul_eq_zero_of_smul (P : R[X]) (h : ∀ r : R, r • P = 0 → r = 0) :
-    ∀ (Q : R[X]), P * Q = 0 → Q = 0 := by
-  intro Q hQ
+theorem eq_zero_of_mul_eq_zero_of_smul (P : R[X]) (h : ∀ r : R, r • P = 0 → r = 0) (Q : R[X])
+    (hQ : P * Q = 0) : Q = 0 := by
   suffices ∀ i, P.coeff i • Q = 0 by
     rw [← leadingCoeff_eq_zero]
     apply h
@@ -666,7 +665,7 @@ theorem eq_zero_of_mul_eq_zero_of_smul (P : R[X]) (h : ∀ r : R, r • P = 0 
     rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]
   · omega
   · rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_zero]
-termination_by Q => Q.natDegree
+termination_by Q.natDegree
 
 open nonZeroDivisors in
 /-- *McCoy theorem*: a polynomial `P : R[X]` is a zerodivisor if and only if there is `a : R`

Mathlib/AlgebraicGeometry/RationalMap.lean

@@ -430,10 +430,10 @@ lemma RationalMap.fromFunctionField_ofFunctionField [IsIntegral X] [LocallyOfFin
 
 lemma RationalMap.eq_of_fromFunctionField_eq [IsIntegral X] (f g : X.RationalMap Y)
     (H : f.fromFunctionField = g.fromFunctionField) : f = g := by
-    obtain ⟨f, rfl⟩ := f.exists_rep
-    obtain ⟨g, rfl⟩ := g.exists_rep
-    refine PartialMap.toRationalMap_eq_iff.mpr ?_
-    exact PartialMap.equiv_of_fromSpecStalkOfMem_eq _ _ _ _ H
+  obtain ⟨f, rfl⟩ := f.exists_rep
+  obtain ⟨g, rfl⟩ := g.exists_rep
+  refine PartialMap.toRationalMap_eq_iff.mpr ?_
+  exact PartialMap.equiv_of_fromSpecStalkOfMem_eq _ _ _ _ H
 
 /--
 Given `S`-schemes `X` and `Y` such that `Y` is locally of finite type and `X` is integral,

Mathlib/Analysis/Analytic/Composition.lean

@@ -355,11 +355,10 @@ theorem id_apply_one' (x : E) {n : ℕ} (h : n = 1) (v : Fin n → E) :
 @[simp]
 theorem id_apply_of_one_lt (x : E) {n : ℕ} (h : 1 < n) :
     (FormalMultilinearSeries.id 𝕜 E x) n = 0 := by
-  cases' n with n
-  · contradiction
-  · cases n
-    · contradiction
-    · rfl
+  match n with
+    | 0 => contradiction
+    | 1 => contradiction
+    | n + 2 => rfl
 
 end
 
@@ -390,22 +389,19 @@ theorem comp_id (p : FormalMultilinearSeries 𝕜 E F) (x : E) : p.comp (id 𝕜
     rw [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply]
     apply ContinuousMultilinearMap.map_coord_zero _ j
     dsimp [applyComposition]
-    rw [id_apply_of_one_lt _ _ _ A]
-    rfl
+    rw [id_apply_of_one_lt _ _ _ A, ContinuousMultilinearMap.zero_apply]
   · simp
 
 @[simp]
 theorem id_comp (p : FormalMultilinearSeries 𝕜 E F) (v0 : Fin 0 → E) :
     (id 𝕜 F (p 0 v0)).comp p = p := by
   ext1 n
-  by_cases hn : n = 0
-  · rw [hn]
-    ext v
+  obtain rfl | n_pos := n.eq_zero_or_pos
+  · ext v
     simp only [comp_coeff_zero', id_apply_zero]
     congr with i
     exact i.elim0
   · dsimp [FormalMultilinearSeries.comp]
-    have n_pos : 0 < n := bot_lt_iff_ne_bot.mpr hn
     rw [Finset.sum_eq_single (Composition.single n n_pos)]
     · show compAlongComposition (id 𝕜 F (p 0 v0)) p (Composition.single n n_pos) = p n
       ext v
@@ -422,8 +418,8 @@ theorem id_comp (p : FormalMultilinearSeries 𝕜 E F) (v0 : Fin 0 → E) :
         have : 0 < b.length := Composition.length_pos_of_pos b n_pos
         omega
       ext v
-      rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A]
-      rfl
+      rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A,
+        ContinuousMultilinearMap.zero_apply, ContinuousMultilinearMap.zero_apply]
     · simp
 
 /-- Variant of `id_comp` in which the zero coefficient is given by an equality hypothesis instead
@@ -548,8 +544,7 @@ def compChangeOfVariables (m M N : ℕ) (i : Σ n, Fin n → ℕ) (hi : i ∈ co
     Σ n, Composition n := by
   rcases i with ⟨n, f⟩
   rw [mem_compPartialSumSource_iff] at hi
-  refine ⟨∑ j, f j, ofFn fun a => f a, fun hi' => ?_, by simp [sum_ofFn]⟩
-  rename_i i
+  refine ⟨∑ j, f j, ofFn fun a => f a, fun {i} hi' => ?_, by simp [sum_ofFn]⟩
   obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn', Set.mem_range] at hi'
   exact (hi.2 j).1
 
@@ -692,8 +687,7 @@ theorem comp_partialSum (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultil
   rintro ⟨k, blocks_fun⟩ H
   apply congr _ (compChangeOfVariables_length 0 M N H).symm
   intros
-  rw [← compChangeOfVariables_blocksFun 0 M N H]
-  rfl
+  rw [← compChangeOfVariables_blocksFun 0 M N H, applyComposition, Function.comp_def]
 
 end FormalMultilinearSeries
 
@@ -803,7 +797,6 @@ theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMult
             ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
           apply ContinuousMultilinearMap.le_opNorm
         _ ≤ ‖compAlongComposition q p c‖ * (r : ℝ) ^ n := by
-          apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
           rw [Finset.prod_const, Finset.card_fin]
           gcongr
           rw [EMetric.mem_ball, edist_zero_eq_enorm] at hy
@@ -817,10 +810,9 @@ theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMult
   have E : HasSum (fun n => (q.comp p) n fun _j => y) (g (f (x + y))) := by
     apply D.sigma
     intro n
-    dsimp [FormalMultilinearSeries.comp]
-    convert hasSum_fintype (α := G) (β := Composition n) _
-    simp only [ContinuousMultilinearMap.sum_apply]
-    rfl
+    simp only [compAlongComposition_apply, FormalMultilinearSeries.comp,
+      ContinuousMultilinearMap.sum_apply]
+    exact hasSum_fintype _
   rw [Function.comp_apply]
   exact E
 
@@ -986,8 +978,9 @@ theorem sigma_composition_eq_iff (i j : Σ a : Composition n, Composition a.leng
   rcases i with ⟨a, b⟩
   rcases j with ⟨a', b'⟩
   rintro ⟨h, h'⟩
-  have H : a = a' := by ext1; exact h
-  induction H; congr; ext1; exact h'
+  obtain rfl : a = a' := by ext1; exact h
+  obtain rfl : b = b' := by ext1; exact h'
+  rfl
 
 /-- Rewriting equality in the dependent type
 `Σ (c : Composition n), Π (i : Fin c.length), Composition (c.blocksFun i)` in
@@ -999,7 +992,7 @@ theorem sigma_pi_composition_eq_iff
   rcases u with ⟨a, b⟩
   rcases v with ⟨a', b'⟩
   dsimp at H
-  have h : a = a' := by
+  obtain rfl : a = a' := by
     ext1
     have :
       map List.sum (ofFn fun i : Fin (Composition.length a) => (b i).blocks) =
@@ -1010,7 +1003,6 @@ theorem sigma_pi_composition_eq_iff
       (ofFn fun i : Fin (Composition.length a) => (b i).blocks.sum) =
         ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this
     simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this
-  induction h
   ext1
   · rfl
   · simp only [heq_eq_eq, ofFn_inj] at H ⊢
@@ -1027,7 +1019,7 @@ def gather (a : Composition n) (b : Composition a.length) : Composition n where
   blocks_pos := by
     rw [forall_mem_map]
     intro j hj
-    suffices H : ∀ i ∈ j, 1 ≤ i by calc
+    suffices H : ∀ i ∈ j, 1 ≤ i from calc
       0 < j.length := length_pos_of_mem_splitWrtComposition hj
       _ ≤ j.sum := length_le_sum_of_one_le _ H
     intro i hi
@@ -1144,7 +1136,7 @@ def sigmaEquivSigmaPi (n : ℕ) :
     ⟨{  blocks := (ofFn fun j => (i.2 j).blocks).flatten
         blocks_pos := by
           simp only [and_imp, List.mem_flatten, exists_imp, forall_mem_ofFn_iff]
-          exact @fun i j hj => Composition.blocks_pos _ hj
+          exact fun {i} j hj => Composition.blocks_pos _ hj
         blocks_sum := by simp [sum_ofFn, Composition.blocks_sum, Composition.sum_blocksFun] },
       { blocks := ofFn fun j => (i.2 j).length
         blocks_pos := by
@@ -1185,15 +1177,13 @@ def sigmaEquivSigmaPi (n : ℕ) :
       ext1
       dsimp [Composition.gather]
       rwa [splitWrtComposition_flatten]
-      simp only [map_ofFn]
-      rfl
+      simp only [map_ofFn, Function.comp_def]
     · rw [Fin.heq_fun_iff]
       · intro i
         dsimp [Composition.sigmaCompositionAux]
         rw [getElem_of_eq (splitWrtComposition_flatten _ _ _)]
         · simp only [List.getElem_ofFn]
-        · simp only [map_ofFn]
-          rfl
+        · simp only [map_ofFn, Function.comp_def]
       · congr
 
 end Composition

Mathlib/Analysis/Calculus/ContDiff/Defs.lean

@@ -96,17 +96,8 @@ derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor ser
 
 noncomputable section
 
-open NNReal Topology Filter
-
-/-
-Porting note: These lines are not required in Mathlib4.
-attribute [local instance 1001]
-  NormedAddCommGroup.toAddCommGroup AddCommGroup.toAddCommMonoid
--/
-
 open Set Fin Filter Function
-
-open scoped ContDiff
+open scoped NNReal Topology ContDiff
 
 universe u uE uF uG uX
 
@@ -413,9 +404,7 @@ theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt (hn : n ≠ ∞) :
       · change
           HasFDerivWithinAt (fun z => (continuousMultilinearCurryFin0 𝕜 E F).symm (f z))
             (FormalMultilinearSeries.unshift (p' y) (f y) 1).curryLeft (v ∩ u) y
-        -- Porting note: needed `erw` here.
-        -- https://github.com/leanprover-community/mathlib4/issues/5164
-        erw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
+        rw [← Function.comp_def _ f, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
         convert (f'_eq_deriv y hy.2).mono inter_subset_right
         rw [← Hp'.zero_eq y hy.1]
         ext z
@@ -826,7 +815,7 @@ theorem contDiffOn_nat_iff_continuousOn_differentiableOn {n : ℕ} (hs : UniqueD
     ContDiffOn 𝕜 n f s ↔
       (∀ m : ℕ, m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
         ∀ m : ℕ, m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s := by
-  rw [show n = ((n : ℕ∞) : WithTop ℕ∞) from rfl, contDiffOn_iff_continuousOn_differentiableOn hs]
+  rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn hs]
   simp
 
 theorem contDiffOn_succ_of_fderivWithin (hf : DifferentiableOn 𝕜 f s)
@@ -895,7 +884,7 @@ alias contDiffOn_succ_iff_hasFDerivWithin := contDiffOn_succ_iff_hasFDerivWithin
 
 theorem contDiffOn_infty_iff_fderivWithin (hs : UniqueDiffOn 𝕜 s) :
     ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s := by
-  rw [show ∞ = ∞ + 1 from rfl, contDiffOn_succ_iff_fderivWithin hs]
+  rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderivWithin hs]
   simp
 
 @[deprecated (since := "2024-11-27")]
@@ -907,12 +896,12 @@ theorem contDiffOn_succ_iff_fderiv_of_isOpen (hs : IsOpen s) :
     ContDiffOn 𝕜 (n + 1) f s ↔
       DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧
       ContDiffOn 𝕜 n (fderiv 𝕜 f) s := by
-  rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn]
-  exact Iff.rfl.and (Iff.rfl.and (contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx))
+  rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn,
+    contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]
 
 theorem contDiffOn_infty_iff_fderiv_of_isOpen (hs : IsOpen s) :
     ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s := by
-  rw [show ∞ = ∞ + 1 from rfl, contDiffOn_succ_iff_fderiv_of_isOpen hs]
+  rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen hs]
   simp
 
 @[deprecated (since := "2024-11-27")]
@@ -1202,7 +1191,7 @@ theorem contDiff_nat_iff_continuous_differentiable {n : ℕ} :
     ContDiff 𝕜 n f ↔
       (∀ m : ℕ, m ≤ n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
         ∀ m : ℕ, m < n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x := by
-  rw [show n = ((n : ℕ∞) : WithTop ℕ∞) from rfl, contDiff_iff_continuous_differentiable]
+  rw [← WithTop.coe_natCast, contDiff_iff_continuous_differentiable]
   simp
 
 /-- If `f` is `C^n` then its `m`-times iterated derivative is continuous for `m ≤ n`. -/
@@ -1231,12 +1220,12 @@ theorem contDiff_succ_iff_fderiv :
 
 theorem contDiff_one_iff_fderiv :
     ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f) := by
-  rw [show (1 : WithTop ℕ∞) = 0 + 1 from rfl, contDiff_succ_iff_fderiv]
+  rw [← zero_add 1, contDiff_succ_iff_fderiv]
   simp
 
 theorem contDiff_infty_iff_fderiv :
     ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f) := by
-  rw [show ∞ = ∞ + 1 from rfl, contDiff_succ_iff_fderiv]
+  rw [← ENat.coe_top_add_one, contDiff_succ_iff_fderiv]
   simp
 
 @[deprecated (since := "2024-11-27")] alias contDiff_top_iff_fderiv := contDiff_infty_iff_fderiv

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -86,7 +86,7 @@ theorem log_zero : log 0 = 0 :=
 theorem log_one : log 1 = 0 :=
   exp_injective <| by rw [exp_log zero_lt_one, exp_zero]
 
-/-- This holds true for all `x : \` because of the junk values `0 / 0 = 0` and `arg 0 = 0`. -/
+/-- This holds true for all `x : ℝ` because of the junk values `0 / 0 = 0` and `log 0 = 0`. -/
 @[simp] lemma log_div_self (x : ℝ) : log (x / x) = 0 := by
   obtain rfl | hx := eq_or_ne x 0 <;> simp [*]
 

Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean

@@ -37,15 +37,15 @@ variable [MonoidalCategory D] [SymmetricCategory D] [MonoidalClosed D]
 section
 variable {R : C ⥤ D} [R.Faithful] [R.Full] {L : D ⥤ C} (adj : L ⊣ R)
 
-/-- The uncurried retraction of the unit in the proof of `4 → 1` in `day_reflection` below. -/
+/-- The uncurried retraction of the unit in the proof of `4 → 1` in `isIso_tfae` below. -/
 private noncomputable def adjRetractionAux
     (c : C) (d : D) [IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))] :
   d ⊗ ((L ⋙ R).obj ((ihom d).obj (R.obj c))) ⟶ (R.obj c) :=
   (β_ _ _).hom ≫ (_ ◁ adj.unit.app _) ≫ adj.unit.app _ ≫
     R.map (inv (L.map (adj.unit.app _ ⊗ adj.unit.app _))) ≫ (L ⋙ R).map (β_ _ _).hom ≫
       (L ⋙ R).map ((ihom.ev _).app _) ≫ inv (adj.unit.app _)
 
-/-- The retraction of the unit in the proof of `4 → 1` in `day_reflection` below. -/
+/-- The retraction of the unit in the proof of `4 → 1` in `isIso_tfae` below. -/
 private noncomputable def adjRetraction (c : C) (d : D)
     [IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))] :
     (L ⋙ R).obj ((ihom d).obj (R.obj c)) ⟶ ((ihom d).obj (R.obj c)) :=