[Merged by Bors] - chore: replace haveI/letI with have/let in tactics when the goal is a prop

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

Mathlib/Algebra/CharP/Algebra.lean

@@ -97,16 +97,16 @@ lemma expChar_of_injective_ringHom
     [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f)
     (q : ℕ) [hR : ExpChar R q] : ExpChar A q := by
   rcases hR with _ | hprime
-  · haveI := charZero_of_injective_ringHom h; exact .zero
-  haveI := charP_of_injective_ringHom h q; exact .prime hprime
+  · have := charZero_of_injective_ringHom h; exact .zero
+  have := charP_of_injective_ringHom h q; exact .prime hprime
 
 /-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
 exponential characteristic `p`. Similar to `RingHom.charZero`. -/
 lemma RingHom.expChar [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
     (H : Function.Injective f) (p : ℕ) [ExpChar A p] : ExpChar R p := by
   cases ‹ExpChar A p› with
-  | zero => haveI := f.charZero; exact .zero
-  | prime hp => haveI := f.charP H p; exact .prime hp
+  | zero => have := f.charZero; exact .zero
+  | prime hp => have := f.charP H p; exact .prime hp
 
 /-- If `R →+* A` is injective, then `R` is of exponential characteristic `p` if and only if `A` is
 also of exponential characteristic `p`. Similar to `RingHom.charZero_iff`. -/

Mathlib/Algebra/CharP/Defs.lean

@@ -156,7 +156,7 @@ namespace ringChar
 variable [NonAssocSemiring R]
 
 lemma spec : ∀ x : ℕ, (x : R) = 0 ↔ ringChar R ∣ x := by
-  letI : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).1
+  let : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).1
   exact CharP.cast_eq_zero_iff R (ringChar R)
 
 lemma eq (p : ℕ) [C : CharP R p] : ringChar R = p :=
@@ -388,7 +388,7 @@ noncomputable def ringExpChar : ℕ := max (ringChar R) 1
 
 lemma ringExpChar.eq (q : ℕ) [h : ExpChar R q] : ringExpChar R = q := by
   rcases h with _ | h
-  · haveI := CharP.ofCharZero R
+  · have := CharP.ofCharZero R
     rw [ringExpChar, ringChar.eq R 0]; rfl
   rw [ringExpChar, ringChar.eq R q]
   exact Nat.max_eq_left h.one_lt.le

Mathlib/Algebra/CharP/Invertible.lean

@@ -65,7 +65,7 @@ def invertibleOfCoprime {n : ℕ} (h : n.Coprime p) :
 
 theorem invOf_eq_of_coprime {n : ℕ} [Invertible (n : R)] (h : n.Coprime p) :
     ⅟(n : R) = n.gcdA p := by
-  letI : Invertible (n : R) := invertibleOfCoprime h
+  let : Invertible (n : R) := invertibleOfCoprime h
   convert! (rfl : ⅟(n : R) = _)
 
 theorem CharP.isUnit_natCast_iff {n : ℕ} (hp : p.Prime) : IsUnit (n : R) ↔ ¬p ∣ n where

Mathlib/Algebra/CharP/Lemmas.lean

@@ -285,7 +285,7 @@ variable (R) [NonAssocRing R]
 /-- The characteristic of a finite ring cannot be zero. -/
 theorem char_ne_zero_of_finite (p : ℕ) [CharP R p] [Finite R] : p ≠ 0 := by
   rintro rfl
-  haveI : CharZero R := charP_to_charZero R
+  have : CharZero R := charP_to_charZero R
   exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))
 
 theorem ringChar_ne_zero_of_finite [Finite R] : ringChar R ≠ 0 :=

Mathlib/Algebra/CharP/LocalRing.lean

@@ -30,7 +30,7 @@ theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [IsLocalRing R] (q :
   apply or_iff_not_imp_left.2
   intro q_pos
   let K := IsLocalRing.ResidueField R
-  haveI RM_char := ringChar.charP K
+  have RM_char := ringChar.charP K
   let r := ringChar K
   let n := q.factorization r
   -- `r := char(R/m)` is either prime or zero:
@@ -58,9 +58,9 @@ theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [IsLocalRing R] (q :
       absurd (by simpa [n_zero] using q_eq_rn) (CharP.char_ne_one R q)
     -- Definition of prime power: `∃ r n, Prime r ∧ 0 < n ∧ r ^ n = q`.
     exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
-  · haveI K_char_p_0 := ringChar.of_eq r_zero
-    haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
-    haveI R_char_zero := RingHom.charZero (IsLocalRing.residue R)
+  · have K_char_p_0 := ringChar.of_eq r_zero
+    have K_char_zero : CharZero K := CharP.charP_to_charZero K
+    have R_char_zero := RingHom.charZero (IsLocalRing.residue R)
     -- Finally, `r = 0` would lead to a contradiction:
     have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
     exact absurd q_zero q_pos

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -278,7 +278,7 @@ theorem nonempty_algebraRat_iff :
     Nonempty (Algebra ℚ R) ↔ ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I) := by
   constructor
   · intro h_alg
-    haveI h_alg' : Algebra ℚ R := h_alg.some
+    have h_alg' : Algebra ℚ R := h_alg.some
     apply of_algebraRat
   · intro h
     apply Nonempty.intro
@@ -333,7 +333,7 @@ theorem split_by_characteristic (h_pos : ∀ p : ℕ, p ≠ 0 → CharP R p →
   | intro p p_charP =>
     by_cases h : p = 0
     · rw [h] at p_charP
-      haveI h0 : CharZero R := CharP.charP_to_charZero R
+      have h0 : CharZero R := CharP.charP_to_charZero R
       exact split_equalCharZero_mixedCharZero R h_equal h_mixed
     · exact h_pos p h p_charP
 

Mathlib/Algebra/CharP/Quotient.lean

@@ -72,5 +72,5 @@ theorem Ideal.Quotient.index_eq_zero (I : Ideal R) : (↑I.toAddSubgroup.index :
   rw [AddSubgroup.index, Nat.card_eq]
   split_ifs with hq; swap
   · simp
-  letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
+  let : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
   exact Nat.cast_card_eq_zero (R ⧸ I)

Mathlib/Algebra/DirectSum/Decomposition.lean

@@ -108,7 +108,7 @@ protected theorem Decomposition.inductionOn {motive : M → Prop} (zero : motive
     (add : ∀ m m' : M, motive m → motive m' → motive (m + m')) : ∀ m, motive m := by
   let ℳ' : ι → AddSubmonoid M := fun i ↦
     (⟨⟨ℳ i, fun x y ↦ AddMemClass.add_mem x y⟩, (ZeroMemClass.zero_mem _)⟩ : AddSubmonoid M)
-  haveI t : DirectSum.Decomposition ℳ' :=
+  have t : DirectSum.Decomposition ℳ' :=
     { decompose' := DirectSum.decompose ℳ
       left_inv := fun _ ↦ (decompose ℳ).left_inv _
       right_inv := fun _ ↦ (decompose ℳ).right_inv _ }

Mathlib/Algebra/DualNumber.lean

@@ -127,7 +127,7 @@ on `R` and its value on `ε`. -/
 lemma ringHom_ext {R' : Type*} [CommSemiring R'] {f g : R[ε] →+* R'}
     (h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε]))
     (hε : f ε = g ε) : f = g := by
-  letI : Algebra R R' := by
+  let : Algebra R R' := by
     letI := f.toAlgebra
     exact Algebra.compHom _ (algebraMap R R[ε])
   let f' : R[ε] →ₐ[R] R' :=

Mathlib/Algebra/EuclideanDomain/Basic.lean

@@ -55,7 +55,7 @@ theorem mod_eq_zero {a b : R} : a % b = 0 ↔ b ∣ a :=
     rw [← div_add_mod a b, h, add_zero]
     exact dvd_mul_right _ _, fun ⟨c, e⟩ => by
     rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
-    haveI := Classical.dec
+    have := Classical.dec
     by_cases b0 : b = 0
     · simp only [b0, zero_mul]
     · rw [mul_div_cancel_left₀ _ b0]⟩

Mathlib/Algebra/Exact/Basic.lean

@@ -90,7 +90,7 @@ may not apply if the zero of `Set.range g` is not definitionally equal to `⟨0,
 lemma iff_rangeFactorization [One P] (hg : 1 ∈ Set.range g) :
     letI : One (Set.range g) := ⟨⟨1, hg⟩⟩
     MulExact f g ↔ MulExact ((↑) : Set.range f → N) (Set.rangeFactorization g) := by
-  letI : One (Set.range g) := ⟨⟨1, hg⟩⟩
+  let : One (Set.range g) := ⟨⟨1, hg⟩⟩
   have : ((1 : Set.range g) : P) = 1 := rfl
   simp [MulExact, Subtype.ext_iff, this]