chore: replace haveI/letI with have/let in tactic proofs of propositions

Archive/Imo/Imo2008Q3.lean

@@ -34,7 +34,7 @@ namespace Imo2008Q3
 
 theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) :
     ∃ n : ℕ, p ∣ n ^ 2 + 1 ∧ (p : ℝ) > 2 * n + sqrt (2 * n) := by
-  haveI := Fact.mk hpp
+  have := Fact.mk hpp
   have hp_mod_4_ne_3 : p % 4 ≠ 3 := by linarith [show p % 4 = 1 from hp_mod_4_eq_1]
   obtain ⟨y, hy⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3
   let m := ZMod.valMinAbs y

Archive/Imo/Imo2019Q2.lean

@@ -275,7 +275,7 @@ theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by
     rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _)
       hwbtw.mem_affineSpan]
     exact cfg.PQ_parallel_AB.direction_eq
-  haveI := someOrientation V
+  have := someOrientation V
   have haQ : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.B cfg.A := by
     rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B]
     rw [Set.pair_comm, Set.insert_comm]
@@ -389,7 +389,7 @@ end Oriented
 
 
 theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, ←
     affineIndependent_iff_not_collinear_set]
   have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
@@ -515,13 +515,13 @@ end Oriented
 
 
 theorem not_collinear_CA₂A₁ : ¬Collinear ℝ ({cfg.C, cfg.A₂, cfg.A₁} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA,
     Set.pair_comm, Set.insert_comm, Set.pair_comm]
   exact cfg.not_collinear_ABC
 
 theorem cospherical_A₁Q₁CA₂ : Cospherical ({cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [Set.insert_comm cfg.Q₁, Set.insert_comm cfg.A₁, Set.pair_comm, Set.insert_comm cfg.A₁,
     Set.pair_comm]
   exact cospherical_of_two_zsmul_oangle_eq_of_not_collinear

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -316,9 +316,9 @@ theorem ballot_problem' :
     rw [div_self]
     exact Nat.cast_add_one_ne_zero p
   · intro q p qp h₁ h₂
-    haveI := isProbabilityMeasure_uniformOn
+    have := isProbabilityMeasure_uniformOn
       (countedSequence_finite p (q + 1)) (countedSequence_nonempty _ _)
-    haveI := isProbabilityMeasure_uniformOn
+    have := isProbabilityMeasure_uniformOn
       (countedSequence_finite (p + 1) q) (countedSequence_nonempty _ _)
     have h₃ : 0 < p + 1 + (q + 1) := Nat.add_pos_left (Nat.succ_pos _) _
     rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
@@ -345,7 +345,7 @@ theorem ballot_problem' :
 theorem ballot_problem :
     ∀ q p, q < p → uniformOn (countedSequence p q) staysPositive = (p - q) / (p + q) := by
   intro q p qp
-  haveI :=
+  have :=
     isProbabilityMeasure_uniformOn (countedSequence_finite p q) (countedSequence_nonempty _ _)
   have :
     (uniformOn (countedSequence p q) staysPositive).toReal =

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -378,7 +378,7 @@ variable (h v)
   direction will intersect one of the neighbouring cubes on the same boundary as `mi`. -/
 theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈ _) j := by
   let i := mi h v; have hi : i ∈ bcubes cs c := mi_mem_bcubes
-  haveI := h.nontrivial_fin
+  have := h.nontrivial_fin
   rcases exists_ne j with ⟨j', hj'⟩
   intro hj
   rcases smallest_onBoundary hj with ⟨x, ⟨hx, h2x⟩, h3x⟩

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -249,7 +249,7 @@ theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : Fa
   have p_dvd_d_pred := (ZMod.natCast_eq_zero_iff _ _).mpr (d - 1).minFac_dvd
   have dpos : 1 ≤ d := by lia
   have d_cast : ↑(d - 1) = (d : ℤ) - 1 := by norm_cast
-  haveI : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩
+  have : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩
   have hp2 : 2 ≤ p := (Fact.out (p := p.Prime)).two_le
   have dmod : (d : ZMod p) = 1 := by
     rw [← Nat.succ_pred_eq_of_pos dpos, Nat.succ_eq_add_one, Nat.pred_eq_sub_one]

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -154,7 +154,7 @@ theorem sq_map_add_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a
 
 theorem sq_map_sub_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) :
     sq i (a - b) = sq i a - sq i b := by
-  haveI : Nonempty ι := ⟨i⟩
+  have : Nonempty ι := ⟨i⟩
   rw [CharTwo.sub_eq_add, CharTwo.sub_eq_add, sq_map_add_char_two]
 
 /-- The quadratic form (metric) is just Euclidean -/

Counterexamples/Phillips.lean

@@ -247,7 +247,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
   -- convenient to formalize the inductive construction.
   let A : Set (Set α) := {t | t.Countable}
   let empty : A := ⟨∅, countable_empty⟩
-  haveI : Nonempty A := ⟨empty⟩
+  have : Nonempty A := ⟨empty⟩
   -- given a countable set `s`, one can find a set `t` in its complement with measure close to
   -- maximal.
   have : ∀ s : A, ∃ t : A, ∀ u : A, f (↑u \ ↑s) ≤ 2 * f (↑t \ ↑s) := by

Counterexamples/SorgenfreyLine.lean

@@ -67,7 +67,7 @@ theorem isOpen_Ici (a : ℝₗ) : IsOpen (Ici a) :=
 
 theorem nhds_basis_Ico (a : ℝₗ) : (𝓝 a).HasBasis (a < ·) (Ico a ·) := by
   rw [TopologicalSpace.nhds_generateFrom]
-  haveI : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype
+  have : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype
   have : (⨅ x : { i // i ≤ a }, 𝓟 (Ici ↑x)) = 𝓟 (Ici a) := by
     refine (IsLeast.isGLB ?_).iInf_eq
     exact ⟨⟨⟨a, le_rfl⟩, rfl⟩, forall_mem_range.2 fun b => principal_mono.2 <| Ici_subset_Ici.2 b.2⟩
@@ -312,7 +312,7 @@ theorem not_separatedNhds_rat_irrational_antidiag :
 /-- Topology on the Sorgenfrey line is not metrizable. -/
 theorem not_metrizableSpace : ¬MetrizableSpace ℝₗ := by
   intro
-  letI := metrizableSpaceMetric ℝₗ
+  let := metrizableSpaceMetric ℝₗ
   exact not_normalSpace_prod inferInstance
 
 /-- Topology on the Sorgenfrey line is not second countable. -/

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -241,8 +241,8 @@ example : ¬UniqueProds ℕ := by
 
 /-- Some Types that do not have `UniqueSums`. -/
 example (n : ℕ) (n2 : 2 ≤ n) : ¬UniqueSums (ZMod n) := by
-  haveI : Fintype (ZMod n) := @ZMod.fintype n ⟨(zero_lt_two.trans_le n2).ne'⟩
-  haveI : Nontrivial (ZMod n) := CharP.nontrivial_of_char_ne_one (one_lt_two.trans_le n2).ne'
+  have : Fintype (ZMod n) := @ZMod.fintype n ⟨(zero_lt_two.trans_le n2).ne'⟩
+  have : Nontrivial (ZMod n) := CharP.nontrivial_of_char_ne_one (one_lt_two.trans_le n2).ne'
   rintro ⟨h⟩
   refine not_not.mpr (h Finset.univ_nonempty Finset.univ_nonempty) ?_
   suffices ∀ x y : ZMod n, ∃ x' y' : ZMod n, x' + y' = x + y ∧ (x' = x → ¬y' = y) by

Mathlib/Algebra/Algebra/Operations.lean

@@ -806,7 +806,7 @@ instance : IdemCommSemiring (Submodule R A) :=
 
 theorem prod_span {ι : Type*} (s : Finset ι) (M : ι → Set A) :
     (∏ i ∈ s, Submodule.span R (M i)) = Submodule.span R (∏ i ∈ s, M i) := by
-  letI := Classical.decEq ι
+  let := Classical.decEq ι
   refine Finset.induction_on s ?_ ?_
   · simp [one_eq_span, Set.singleton_one]
   · intro _ _ H ih

Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean

@@ -24,8 +24,8 @@ theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDo
       ⟨⟨⊥, ⊤, fun he =>
           Nat.not_prime_one ((Subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩
     eq_bot_or_eq_top := fun K => by
-      haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
-      letI := divisionRingOfFiniteDimensional F K
+      have : FiniteDimensional _ _ := .of_finrank_pos hp.pos
+      let := divisionRingOfFiniteDimensional F K
       refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_
       · exact fun h' => Subalgebra.eq_bot_of_finrank_one h'
       · exact

Mathlib/Algebra/Algebra/Subalgebra/Rank.lean

@@ -35,11 +35,11 @@ variable [Module.Free R A] [Module.Free A (Algebra.adjoin A (B : Set S))]
 theorem rank_sup_eq_rank_left_mul_rank_of_free :
     Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank A (Algebra.adjoin A (B : Set S)) := by
   rcases subsingleton_or_nontrivial R with _ | _
-  · haveI := Module.subsingleton R S; simp
+  · have := Module.subsingleton R S; simp
   nontriviality S using rank_subsingleton'
-  letI : Algebra A (Algebra.adjoin A (B : Set S)) := Subalgebra.algebra _
-  letI : SMul A (Algebra.adjoin A (B : Set S)) := Algebra.toSMul
-  haveI : IsScalarTower R A (Algebra.adjoin A (B : Set S)) :=
+  let : Algebra A (Algebra.adjoin A (B : Set S)) := Subalgebra.algebra _
+  let : SMul A (Algebra.adjoin A (B : Set S)) := Algebra.toSMul
+  have : IsScalarTower R A (Algebra.adjoin A (B : Set S)) :=
     IsScalarTower.of_algebraMap_eq (congrFun rfl)
   rw [rank_mul_rank R A (Algebra.adjoin A (B : Set S))]
   change _ = Module.rank R ((Algebra.adjoin A (B : Set S)).restrictScalars R)

Mathlib/Algebra/AlgebraicCard.lean

@@ -31,7 +31,7 @@ namespace Algebraic
 
 theorem infinite_of_charZero (R A : Type*) [CommRing R] [Ring A] [Algebra R A]
     [CharZero A] : { x : A | IsAlgebraic R x }.Infinite := by
-  letI := MulActionWithZero.nontrivial R A
+  let := MulActionWithZero.nontrivial R A
   exact infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_nat
 
 theorem aleph0_le_cardinalMk_of_charZero (R A : Type*) [CommRing R] [Ring A]

Mathlib/Algebra/BigOperators/Associated.lean

@@ -178,7 +178,7 @@ theorem prod_eq_one_iff {p : Multiset (Associates M)} :
     (by simp +contextual [mul_eq_one, or_imp, forall_and])
 
 theorem prod_le_prod {p q : Multiset (Associates M)} (h : p ≤ q) : p.prod ≤ q.prod := by
-  haveI := Classical.decEq (Associates M)
+  have := Classical.decEq (Associates M)
   suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
   suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
   exact mul_mono (le_refl p.prod) one_le

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -226,9 +226,9 @@ theorem finprod_true (f : True → M) : ∏ᶠ i, f i = f trivial :=
 theorem finprod_eq_dif {p : Prop} [Decidable p] (f : p → M) :
     ∏ᶠ i, f i = if h : p then f h else 1 := by
   split_ifs with h
-  · haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
+  · have : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
     exact finprod_unique f
-  · haveI : IsEmpty p := ⟨h⟩
+  · have : IsEmpty p := ⟨h⟩
     exact finprod_of_isEmpty f
 
 @[to_additive]
@@ -1065,7 +1065,7 @@ over `a ∈ ⋃ i ∈ I, t i` is equal to the product over `i ∈ I` of the prod
       over `a ∈ t i`. -/]
 theorem finprod_mem_biUnion {I : Set ι} {t : ι → Set α} (h : I.PairwiseDisjoint t) (hI : I.Finite)
     (ht : ∀ i ∈ I, (t i).Finite) : ∏ᶠ a ∈ ⋃ x ∈ I, t x, f a = ∏ᶠ i ∈ I, ∏ᶠ j ∈ t i, f j := by
-  haveI := hI.fintype
+  have := hI.fintype
   rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
   exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]
 

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -393,7 +393,7 @@ lemma prod_congr_of_eq_on_inter {ι M : Type*} {s₁ s₂ : Finset ι} {f g : ι
 @[to_additive]
 theorem prod_eq_mul_of_mem {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s)
     (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : ∏ x ∈ s, f x = f a * f b := by
-  haveI := Classical.decEq ι; let s' := ({a, b} : Finset ι)
+  have := Classical.decEq ι; let s' := ({a, b} : Finset ι)
   have hu : s' ⊆ s := by grind
   have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by grind
   rw [← Finset.prod_subset hu hf]
@@ -403,7 +403,7 @@ theorem prod_eq_mul_of_mem {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈
 theorem prod_eq_mul {s : Finset ι} {f : ι → M} (a b : ι) (hn : a ≠ b)
     (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) (ha : a ∉ s → f a = 1) (hb : b ∉ s → f b = 1) :
     ∏ x ∈ s, f x = f a * f b := by
-  haveI := Classical.decEq ι; by_cases h₁ : a ∈ s <;> by_cases h₂ : b ∈ s
+  have := Classical.decEq ι; by_cases h₁ : a ∈ s <;> by_cases h₂ : b ∈ s
   · exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀
   · rw [hb h₂, mul_one]
     apply prod_eq_single_of_mem a h₁

Mathlib/Algebra/Category/Grp/Images.lean

@@ -60,14 +60,14 @@ noncomputable def image.lift (F' : MonoFactorisation f) : image f ⟶ F'.I :=
   ofHom
   { toFun := (fun x => F'.e (Classical.indefiniteDescription _ x.2).1 : image f → F'.I)
     map_zero' := by
-      haveI := F'.m_mono
+      have := F'.m_mono
       apply injective_of_mono F'.m
       change (F'.e ≫ F'.m) _ = _
       rw [F'.fac, map_zero]
       exact (Classical.indefiniteDescription (fun y => f y = 0) _).2
     map_add' := by
       intro x y
-      haveI := F'.m_mono
+      have := F'.m_mono
       apply injective_of_mono F'.m
       rw [map_add]
       change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -427,7 +427,7 @@ lemma hom_ext {M : ModuleCat R} {N : ModuleCat S}
     {α β : (extendScalars f).obj M ⟶ N}
     (h : ∀ (m : M), α ((1 : S) ⊗ₜ m) = β ((1 : S) ⊗ₜ m)) : α = β := by
   apply (restrictScalars f).map_injective
-  letI := f.toAlgebra
+  let := f.toAlgebra
   ext : 1
   apply TensorProduct.ext'
   intro (s : S) m
@@ -765,7 +765,7 @@ def homEquiv {X : ModuleCat R} {Y : ModuleCat S} :
   toFun := HomEquiv.toRestrictScalars.{u₁, u₂, v} f
   invFun := HomEquiv.fromExtendScalars.{u₁, u₂, v} f
   left_inv g := by
-    letI m1 : Module R S := Module.compHom S f; letI m2 : Module R Y := Module.compHom Y f
+    let m1 : Module R S := Module.compHom S f; let m2 : Module R Y := Module.compHom Y f
     apply hom_ext
     apply LinearMap.ext; intro z
     induction z using TensorProduct.induction_on with
@@ -779,7 +779,7 @@ def homEquiv {X : ModuleCat R} {Y : ModuleCat S} :
       rfl
     | add _ _ ih1 ih2 => rw [map_add, map_add, ih1, ih2]
   right_inv g := by
-    letI m1 : Module R S := Module.compHom S f; letI m2 : Module R Y := Module.compHom Y f
+    let m1 : Module R S := Module.compHom S f; let m2 : Module R Y := Module.compHom Y f
     ext x
     rw [HomEquiv.toRestrictScalars_hom_apply]
     -- This needs to be `erw` because of some unfolding in `fromExtendScalars`
@@ -801,7 +801,7 @@ def Unit.map {X : ModuleCat R} : X ⟶ (extendScalars f ⋙ restrictScalars f).o
   { toFun := fun x => (1 : S) ⊗ₜ[R,f] x
     map_add' := fun x x' => by dsimp; rw [TensorProduct.tmul_add]
     map_smul' := fun r x => by
-      letI m1 : Module R S := Module.compHom S f
+      let m1 : Module R S := Module.compHom S f
       dsimp; rw [← TensorProduct.smul_tmul, TensorProduct.smul_tmul'] }
 
 /--
@@ -860,9 +860,9 @@ def counit : restrictScalars.{max v u₂, u₁, u₂} f ⋙ extendScalars f ⟶
   app _ := Counit.map.{u₁, u₂, v} f
   naturality Y Y' g := by
     -- Porting note: this is very annoying; fix instances in concrete categories
-    letI m1 : Module R S := Module.compHom S f
-    letI m2 : Module R Y := Module.compHom Y f
-    letI m2 : Module R Y' := Module.compHom Y' f
+    let m1 : Module R S := Module.compHom S f
+    let m2 : Module R Y := Module.compHom Y f
+    let m2 : Module R Y' := Module.compHom Y' f
     ext z
     induction z using TensorProduct.induction_on with
     | zero => rw [map_zero, map_zero]

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

@@ -175,8 +175,8 @@ noncomputable def desc : CommRingCat.KaehlerDifferential f ⟶ M :=
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma desc_d (b : B) : D.desc (CommRingCat.KaehlerDifferential.d b) = D.d b := by
-  letI := f.hom.toAlgebra
-  letI := Module.compHom M f.hom
+  let := f.hom.toAlgebra
+  let := Module.compHom M f.hom
   apply D.liftKaehlerDifferential_comp_D
 
 end ModuleCat.Derivation

Mathlib/Algebra/Category/ModuleCat/Free.lean

@@ -172,7 +172,7 @@ theorem free_shortExact [Module.Free R S.X₁] [Module.Free R S.X₃] :
 theorem free_shortExact_rank_add [Module.Free R S.X₁] [Module.Free R S.X₃]
     [StrongRankCondition R] :
     Module.rank R S.X₂ = Module.rank R S.X₁ + Module.rank R S.X₃ := by
-  haveI := free_shortExact hS'
+  have := free_shortExact hS'
   rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R S.X₁,
     Module.Free.rank_eq_card_chooseBasisIndex R S.X₃, Cardinal.add_def, Cardinal.eq]
   exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS'

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -64,7 +64,7 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) :=
     (fun s => ofHom <| (LinearMap.range f.hom).liftQ (Cofork.π s).hom <|
       LinearMap.range_le_ker_iff.2 <| ModuleCat.hom_ext_iff.mp <| CokernelCofork.condition s)
     (fun s => hom_ext <| (LinearMap.range f.hom).liftQ_mkQ (Cofork.π s).hom _) fun s m h => by
-    haveI : Epi (ofHom f.hom.range.mkQ) :=
+    have : Epi (ofHom f.hom.range.mkQ) :=
       (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)
     apply (cancel_epi (ofHom f.hom.range.mkQ)).1
     exact h

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

@@ -111,7 +111,7 @@ noncomputable instance : (restrictScalars f).LaxMonoidal :=
 @[simp]
 lemma restrictScalars_η (r : R) :
     ε (restrictScalars f) r = f r := by
-  letI := f.toAlgebra
+  let := f.toAlgebra
   dsimp [Adjunction.rightAdjointLaxMonoidal_ε]
   rw [extendRestrictScalarsAdj_homEquiv_apply, extendScalars_η]
   erw [AlgebraTensorModule.rid_tmul]

Mathlib/Algebra/Category/ModuleCat/Stalk.lean

@@ -136,7 +136,7 @@ lemma IsColimit.ι_smul {cR : Cocone R} (hcR : IsColimit cR) {cM : Cocone M}
     letI := IsColimit.module R M H hcR hcM
     cM.ι.app i (r • m) =
       HSMul.hSMul (α := cR.pt) (β := cM.pt) (cR.ι.app i r) (cM.ι.app i m) := by
-  letI := filteredColimitsModule R M H
+  let := filteredColimitsModule R M H
   let α := IsColimit.coconePointUniqueUpToIso hcM
     (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
   let β := IsColimit.coconePointUniqueUpToIso hcR

Mathlib/Algebra/Category/Ring/Epi.lean

@@ -34,7 +34,7 @@ lemma CommRingCat.epi_iff_epi {R S : Type u} [CommRing R] [CommRing S] [Algebra
           simp only [Algebra.algebraMap_eq_smul_one, smul_tmul])
     exact RingHom.congr_fun (congrArg Hom.hom this)
   · refine fun H ↦ ⟨fun {T} f g e ↦ ?_⟩
-    letI : Algebra R T := (ofHom (algebraMap R S) ≫ g).hom.toAlgebra
+    let : Algebra R T := (ofHom (algebraMap R S) ≫ g).hom.toAlgebra
     let f' : S →ₐ[R] T := ⟨f.hom, RingHom.congr_fun (congrArg Hom.hom e)⟩
     let g' : S →ₐ[R] T := ⟨g.hom, fun _ ↦ rfl⟩
     ext s

Mathlib/Algebra/Category/Ring/FinitePresentation.lean

@@ -83,7 +83,7 @@ lemma RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit (hf : f.hom.Finit
     ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i := by
   classical
   have hc' := isColimitOfPreserves (forget _) hc
-  letI := f.hom.toAlgebra
+  let := f.hom.toAlgebra
   obtain ⟨n, hn⟩ := hf
   let P := CommRingCat.of (MvPolynomial (Fin n) R)
   let iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C

Mathlib/Algebra/Category/Ring/LinearAlgebra.lean

@@ -31,7 +31,7 @@ lemma nontrivial_of_isPushout_of_isField {A B C D : CommRingCat.{u}}
     (hA : IsField A) {f : A ⟶ B} {g : A ⟶ C} {inl : B ⟶ D} {inr : C ⟶ D}
     [Nontrivial B] [Nontrivial C]
     (h : IsPushout f g inl inr) : Nontrivial D := by
-  letI : Field A := hA.toField
+  let : Field A := hA.toField
   algebraize [f.hom, g.hom]
   let e : D ≅ .of (B ⊗[A] C) :=
     IsColimit.coconePointUniqueUpToIso h.isColimit (CommRingCat.pushoutCoconeIsColimit A B C)

Mathlib/Algebra/Central/Basic.lean

@@ -47,7 +47,7 @@ lemma baseField_essentially_unique
     [Algebra k K] [Algebra K D] [Algebra k D] [IsScalarTower k K D]
     [IsCentral k D] :
     Function.Bijective (algebraMap k K) := by
-  haveI : IsCentral K D :=
+  have : IsCentral K D :=
   { out := fun x ↦ show x ∈ Subalgebra.center k D → _ by
       simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]
       rintro x rfl