merge upstream/master

Author: kim-em

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 0efe1f98dd7e3b632b596b0360dd01cb7f4bc4c7
+    default: 650f6b52cdb1e35e704c85daad0a6c6d7a02e05c
   path:
     description: Checkout destination path.
     required: false

Mathlib.lean

@@ -5488,6 +5488,7 @@ public import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
 public import Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
 public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
 public import Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
+public import Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
 public import Mathlib.MeasureTheory.Measure.WithDensity
 public import Mathlib.MeasureTheory.Measure.WithDensityFinite
 public import Mathlib.MeasureTheory.Order.Group.Lattice
@@ -6165,6 +6166,7 @@ public import Mathlib.Probability.Kernel.Composition.RadonNikodym
 public import Mathlib.Probability.Kernel.CondDistrib
 public import Mathlib.Probability.Kernel.Condexp
 public import Mathlib.Probability.Kernel.Defs
+public import Mathlib.Probability.Kernel.Deterministic
 public import Mathlib.Probability.Kernel.Disintegration.Basic
 public import Mathlib.Probability.Kernel.Disintegration.CDFToKernel
 public import Mathlib.Probability.Kernel.Disintegration.CondCDF
@@ -6757,6 +6759,8 @@ public import Mathlib.RingTheory.QuotSMulTop
 public import Mathlib.RingTheory.Radical
 public import Mathlib.RingTheory.Radical.Basic
 public import Mathlib.RingTheory.Radical.NatInt
+public import Mathlib.RingTheory.RamificationInertia.Inertia
+public import Mathlib.RingTheory.RamificationInertia.Ramification
 public import Mathlib.RingTheory.ReesAlgebra
 public import Mathlib.RingTheory.Regular.Category
 public import Mathlib.RingTheory.Regular.Depth
@@ -7639,6 +7643,7 @@ public import Mathlib.Topology.Convenient.Category
 public import Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
 public import Mathlib.Topology.Convenient.GeneratedBy
 public import Mathlib.Topology.Convenient.HomSpace
+public import Mathlib.Topology.Convenient.OpenClosed
 public import Mathlib.Topology.Covering
 public import Mathlib.Topology.Covering.AddCircle
 public import Mathlib.Topology.Covering.Basic

Mathlib/Algebra/Algebra/Equiv.lean

@@ -174,15 +174,17 @@ def toAlgHom : A₁ →ₐ[R] A₂ :=
     map_one' := map_one e
     map_zero' := map_zero e }
 
-@[simp]
+instance : CoeOut (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂) where coe := AlgEquiv.toAlgHom
+
+@[deprecated "Now a syntactic equality" (since := "2026-04-29"), nolint synTaut]
 theorem toAlgHom_eq_coe : e.toAlgHom = e :=
   rfl
 
 theorem toAlgHom_apply (x : A₁) : e.toAlgHom x = e x :=
   rfl
 
 @[simp, norm_cast]
-theorem coe_algHom : DFunLike.coe (e.toAlgHom) = DFunLike.coe e :=
+theorem coe_algHom : DFunLike.coe e.toAlgHom = DFunLike.coe e :=
   rfl
 
 theorem coe_algHom_injective : Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ →ₐ[R] A₂) :=
@@ -405,10 +407,10 @@ def arrowCongr (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (A
   toFun f := (e₂.toAlgHom.comp f).comp e₁.symm.toAlgHom
   invFun f := (e₂.symm.toAlgHom.comp f).comp e₁.toAlgHom
   left_inv f := by
-    simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, symm_comp]
+    simp only [AlgHom.comp_assoc, symm_comp]
     simp only [← AlgHom.comp_assoc, symm_comp, AlgHom.id_comp, AlgHom.comp_id]
   right_inv f := by
-    simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, comp_symm]
+    simp only [AlgHom.comp_assoc, comp_symm]
     simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]
 
 theorem arrowCongr_comp (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂')
@@ -573,7 +575,7 @@ lemma toLinearMap_ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective
 
 @[simp]
 lemma toAlgHom_ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) :
-    AlgHomClass.toAlgHom (ofBijective f hf) = f := rfl
+    (ofBijective f hf).toAlgHom = f := rfl
 
 lemma ofBijective_apply_symm_apply (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) (x : A₂) :
     f ((ofBijective f hf).symm x) = x :=

Mathlib/Algebra/Algebra/Hom.lean

@@ -71,9 +71,6 @@ def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →
   toFun := f
   commutes' := AlgHomClass.commutes f
 
-instance coeTC {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
-  ⟨AlgHomClass.toAlgHom⟩
-
 end AlgHomClass
 
 namespace AlgHom
@@ -111,7 +108,7 @@ initialize_simps_projections AlgHom (toFun → apply)
 
 @[simp]
 protected theorem coe_coe {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
-    ⇑(f : A →ₐ[R] B) = f :=
+    ⇑(AlgHomClass.toAlgHom f : A →ₐ[R] B) = f :=
   rfl
 
 @[simp]

Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean

@@ -117,7 +117,7 @@ lemma centralizer_coe_image_includeRight_eq_center_tensorProduct
       ⟨fun h b hb ↦ (Algebra.TensorProduct.comm R A B).symm.injective <| by aesop, fun h b hb ↦
         (Algebra.TensorProduct.comm R A B).injective <| by aesop⟩
   · ext x
-    simp only [AlgHom.mem_range, AlgEquiv.toAlgHom_eq_coe, mem_comap, AlgHom.coe_coe]
+    simp only [AlgHom.mem_range, mem_comap, AlgEquiv.coe_algHom]
     constructor
     · rintro ⟨x, rfl⟩
       exact ⟨(Algebra.TensorProduct.comm R _ _) x,

Mathlib/Algebra/Category/CommBialgCat.lean

@@ -97,7 +97,7 @@ initialize_simps_projections Hom (hom' → hom)
 The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`.
 -/
 
-@[simp] lemma hom_id : (𝟙 A : A ⟶ A).hom = AlgHom.id R A := rfl
+@[simp] lemma hom_id : (𝟙 A : A ⟶ A).hom = .id R A := rfl
 @[simp] lemma hom_comp (f : A ⟶ B) (g : B ⟶ C) : (f ≫ g).hom = g.hom.comp f.hom := rfl
 
 lemma id_apply (A : CommBialgCat.{v} R) (a : A) : (𝟙 A : A ⟶ A) a = a := by simp
@@ -132,13 +132,14 @@ instance : Bialgebra R ((forget (CommBialgCat R)).obj A) := inferInstanceAs <| B
 
 instance hasForgetToCommAlgCat : HasForget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R) where
   forget₂.obj M := .of R M
-  forget₂.map f := CommAlgCat.ofHom f.hom
+  forget₂.map f := CommAlgCat.ofHom f.hom.toAlgHom
 
 @[simp] lemma forget₂_commAlgCat_obj (A : CommBialgCat.{v} R) :
     (forget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R)).obj A = .of R A := rfl
 
 @[simp] lemma forget₂_commAlgCat_map (f : A ⟶ B) :
-    (forget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R)).map f = CommAlgCat.ofHom f.hom := rfl
+    (forget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R)).map f =
+      CommAlgCat.ofHom f.hom.toAlgHom := rfl
 
 /-- Forgetting to the underlying type and then building the bundled object returns the original
 bialgebra. -/
@@ -203,7 +204,7 @@ instance {A : Type u} [CommRing A] [Bialgebra R A] [IsCocomm R A] :
   mul_comm := by ext; exact comm_comul R _
 
 instance {A B : Type u} [CommRing A] [Bialgebra R A] [CommRing B] [Bialgebra R B]
-    (f : A →ₐc[R] B) : IsMonHom (CommAlgCat.ofHom (f : A →ₐ[R] B)).op where
+    (f : A →ₐc[R] B) : IsMonHom (CommAlgCat.ofHom f.toAlgHom).op where
 
 instance (A : (CommAlgCat R)ᵒᵖ) [MonObj A] : Bialgebra R A.unop :=
   .ofAlgHom μ[A].unop.hom η[A].unop.hom
@@ -218,7 +219,7 @@ variable (R) in
   unitIso_inv_app counitIso_hom_app counitIso_inv_app]
 def commBialgCatEquivComonCommAlgCat : CommBialgCat R ≌ (Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ where
   functor.obj A := .op <| .mk <| .op <| .of R A
-  functor.map {A B} f := .op <| .mk' <| .op <| CommAlgCat.ofHom f.hom
+  functor.map {A B} f := .op <| .mk' <| .op <| CommAlgCat.ofHom <| f.hom.toAlgHom
   inverse.obj A := .of R A.unop.X.unop
   inverse.map {A B} f := CommBialgCat.ofHom <| .ofAlgHom f.unop.hom.unop.hom
     congr(($(IsMonHom.one_hom (f := f.unop.hom))).unop.hom)
@@ -231,12 +232,12 @@ def commBialgCatEquivComonCommAlgCat : CommBialgCat R ≌ (Mon (CommAlgCat R)ᵒ
 @[simp]
 lemma commBialgCatEquivComonCommAlgCat_functor_map_unop_hom {A B : CommBialgCat R} (f : A ⟶ B) :
   ((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom =
-    (CommAlgCat.ofHom (AlgHomClass.toAlgHom f.hom)).op := rfl
+    (CommAlgCat.ofHom f.hom.toAlgHom).op := rfl
 
 @[simp]
 lemma commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom
     {A B : (Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ} (f : A ⟶ B) :
-  AlgHomClass.toAlgHom ((commBialgCatEquivComonCommAlgCat R).inverse.map f).hom =
+  ((commBialgCatEquivComonCommAlgCat R).inverse.map f).hom.toAlgHom =
     f.unop.hom.unop.hom := rfl
 
 instance {A : CommBialgCat.{u} R} [IsCocomm R A] :

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -486,14 +486,13 @@ end Unbundled
 variable (M : ModuleCat.{v} R)
 
 /-- If `M` is an `R`-module, then the set of `R`-linear maps `S →ₗ[R] M` is an `S`-module with
-scalar multiplication defined by `s • l := x ↦ l (x • s)` -/
+scalar multiplication defined by `s • l := x ↦ l (x • s)`.
+
+This is an implementation detail: use `(coextendScalars f).obj` instead.
+-/
 def obj' : ModuleCat S :=
   of _ ((restrictScalars f).obj (of _ S) →ₗ[R] M)
 
-set_option backward.inferInstanceAs.wrap.data false in
-instance : CoeFun (obj' f M) fun _ => S → M :=
-  inferInstanceAs <| CoeFun ((restrictScalars f).obj (of _ S) →ₗ[R] M) _
-
 /-- If `M, M'` are `R`-modules, then any `R`-linear map `g : M ⟶ M'` induces an `S`-linear map
 `(S →ₗ[R] M) ⟶ (S →ₗ[R] M')` defined by `h ↦ g ∘ h` -/
 @[simps!]
@@ -509,6 +508,8 @@ end CoextendScalars
 For any rings `R, S` and a ring homomorphism `f : R →+* S`, there is a functor from `R`-module to
 `S`-module defined by `M ↦ (S →ₗ[R] M)` where `S` is considered as an `R`-module via restriction of
 scalars and `g : M ⟶ M'` is sent to `h ↦ g ∘ h`.
+
+The definition of `(coextendScalars f).obj` is given by `CoextendScalars.equiv`.
 -/
 def coextendScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
     ModuleCat R ⥤ ModuleCat S where
@@ -521,9 +522,22 @@ namespace CoextendScalars
 
 variable {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S)
 
-set_option backward.inferInstanceAs.wrap.data false in
-instance (M : ModuleCat R) : CoeFun ((coextendScalars f).obj M) fun _ => S → M :=
-  inferInstanceAs <| CoeFun (CoextendScalars.obj' f M) _
+/-- The carrier of `(coextendScalars f).obj M` is `S →ₗ[R] M` where `S` is considered as an
+`R`-module via restriction of scalars. -/
+def equiv (M : ModuleCat R) :
+    (coextendScalars f).obj M ≃ₗ[S] ((restrictScalars f).obj (of _ S) →ₗ[R] M) where
+  toFun f := f
+  invFun f := f
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+instance (M : ModuleCat R) : CoeFun ((coextendScalars f).obj M) fun _ => S → M where
+  coe g := equiv f M g
+
+variable {f} in
+@[ext] lemma ext {M : ModuleCat R} {g g' : (coextendScalars f).obj M}
+    (h : CoextendScalars.equiv f M g = CoextendScalars.equiv f M g') :
+    g = g' := (CoextendScalars.equiv f M).injective h
 
 theorem smul_apply (M : ModuleCat R) (g : (coextendScalars f).obj M) (s s' : S) :
     (s • g) s' = g (s' * s) :=
@@ -547,20 +561,19 @@ corresponds to `Y ⟶ (coextendScalars f).obj X` by sending `y ↦ (s ↦ g (s 
 def HomEquiv.fromRestriction {X : ModuleCat R} {Y : ModuleCat S}
     (g : (restrictScalars f).obj Y ⟶ X) : Y ⟶ (coextendScalars f).obj X :=
   ofHom
-  { toFun := fun y : Y =>
+  { toFun := fun y : Y => (CoextendScalars.equiv _ _).symm
       { toFun := fun s : S => g <| (s • y : Y)
-        map_add' := fun s1 s2 : S => by simp only [add_smul]; rw [map_add]
+        map_add' := fun s1 s2 : S => by simp [add_smul]
         map_smul' := fun r (s : S) => by
           -- Porting note: dsimp clears out some rw's but less eager to apply others with Lean 4
           dsimp
           rw [← g.hom.map_smul]
-          erw [smul_eq_mul, mul_smul]
-          rfl }
-    map_add' := fun y1 y2 : Y =>
-      LinearMap.ext fun s : S => by
-        simp [smul_add, map_add]
-    map_smul' := fun (s : S) (y : Y) => LinearMap.ext fun t : S => by
-        simp [mul_smul] }
+          erw [smul_eq_mul]
+          simp [mul_smul] }
+    map_add' (y1 y2 : Y) := (CoextendScalars.equiv _ _).injective <|
+      LinearMap.ext fun s : S => by simp
+    map_smul' (s : S) (y : Y) := (CoextendScalars.equiv _ _).injective <|
+      LinearMap.ext fun t : S => by simp [mul_smul] }
 
 /-- This should be autogenerated by `@[simps]` but we need to give `s` the correct type here. -/
 @[simp] lemma HomEquiv.fromRestriction_hom_apply_apply {X : ModuleCat R} {Y : ModuleCat S}
@@ -576,13 +589,11 @@ def HomEquiv.toRestriction {X : ModuleCat R} {Y : ModuleCat S} (g : Y ⟶ (coext
   -- TODO: after https://github.com/leanprover-community/mathlib4/pull/19511 we need to hint `(X := ...)`.
   -- This suggests `restrictScalars` needs to be redesigned.
   ofHom (X := (restrictScalars f).obj Y)
-  { toFun := fun y : Y => (g y) (1 : S)
-    map_add' := fun x y => by dsimp; rw [g.hom.map_add, LinearMap.add_apply]
-    map_smul' := fun r (y : Y) => by
-      dsimp
+  { toFun y := (g y) (1 : S)
+    map_add' x y := by simp
+    map_smul' r (y : Y) := by
       rw [← map_smul]
-      erw [smul_eq_mul, mul_one, map_smul]
-      rw [CoextendScalars.smul_apply (s := f r) (g := g y) (s' := 1), one_mul]
+      erw [smul_eq_mul]
       simp }
 
 /-- This should be autogenerated by `@[simps]` but we need to give `1` the correct type here. -/
@@ -594,28 +605,18 @@ set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- Auxiliary definition for `unit'`, to address timeouts. -/
 def app' (Y : ModuleCat S) : Y →ₗ[S] (restrictScalars f ⋙ coextendScalars f).obj Y :=
-  { toFun := fun y : Y =>
-      { toFun := fun s : S => (s • y : Y)
-        map_add' := fun _ _ => add_smul _ _ _
-        map_smul' := fun r (s : S) => by
-          dsimp only [AddHom.toFun_eq_coe, AddHom.coe_mk, RingHom.id_apply]
-          erw [smul_eq_mul, mul_smul]
-          simp }
-    map_add' := fun y1 y2 =>
+  { toFun y := (CoextendScalars.equiv _ _).symm
+      { toFun (s : S) := s • y
+        map_add' _ _ := add_smul _ _ _
+        map_smul' r (s : S) := by
+          erw [smul_eq_mul]
+          simp [mul_smul] }
+    map_add' y1 y2 := (CoextendScalars.equiv _ _).injective <|
       LinearMap.ext fun s : S => by
-        -- Porting note: double dsimp seems odd
-        dsimp only [AddHom.toFun_eq_coe, AddHom.coe_mk, RingHom.id_apply,
-          RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
-          MonoidHom.coe_coe, ZeroHom.coe_mk, smul_eq_mul, id_eq, eq_mpr_eq_cast, cast_eq,
-          Functor.comp_obj]
-        rw [LinearMap.add_apply, LinearMap.coe_mk, LinearMap.coe_mk, LinearMap.coe_mk]
-        dsimp
-        rw [smul_add]
-    map_smul' := fun s (y : Y) => LinearMap.ext fun t : S => by
-      -- Porting note: used to be simp [mul_smul]
-      rw [RingHom.id_apply, LinearMap.coe_mk, CoextendScalars.smul_apply', LinearMap.coe_mk]
-      dsimp
-      rw [mul_smul] }
+        simp [smul_add]
+    map_smul' s (y : Y) := (CoextendScalars.equiv _ _).injective <|
+      LinearMap.ext fun t : S => by
+        simp [mul_smul] }
 
 /--
 The natural transformation from identity functor to the composition of restriction and coextension
@@ -625,7 +626,7 @@ of scalars.
 protected noncomputable def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙ coextendScalars f where
   app Y := ofHom (app' f Y)
   naturality Y Y' g :=
-    hom_ext <| LinearMap.ext fun y : Y => LinearMap.ext fun s : S => by
+    hom_ext <| LinearMap.ext fun y : Y => CoextendScalars.ext <| LinearMap.ext fun s : S => by
       -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): previously simp [CoextendScalars.map_apply]
       simp only [ModuleCat.hom_comp, Functor.id_map, Functor.id_obj,
         Functor.comp_map]
@@ -641,16 +642,14 @@ protected noncomputable def counit' : coextendScalars f ⋙ restrictScalars f 
   -- TODO: after https://github.com/leanprover-community/mathlib4/pull/19511 we need to hint `(X := ...)`.
   -- This suggests `restrictScalars` needs to be redesigned.
   app X := ofHom (X := (restrictScalars f).obj ((coextendScalars f).obj X))
-    { toFun := fun g => g.toFun (1 : S)
-      map_add' := fun x1 x2 => by
-        dsimp
-        rw [LinearMap.add_apply]
-      map_smul' := fun r (g : (restrictScalars f).obj ((coextendScalars f).obj X)) => by
+    { toFun g := CoextendScalars.equiv f X g (1 : S)
+      map_add' x1 x2 := by simp
+      map_smul' r g := by
         dsimp
         rw [CoextendScalars.smul_apply, one_mul, ← map_smul]
         congr
         change f r = f r • (1 : S)
-        rw [smul_eq_mul (f r) 1, mul_one] }
+        simp }
 
 end RestrictionCoextensionAdj
 
@@ -664,16 +663,12 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S]
     homEquiv := fun X Y ↦
       { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f
         invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f
-        left_inv := fun g => by ext; simp
-        right_inv := fun g => hom_ext <| LinearMap.ext fun x => LinearMap.ext fun s : S => by
-          -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): once just simp
-          rw [RestrictionCoextensionAdj.HomEquiv.fromRestriction_hom_apply_apply,
-              RestrictionCoextensionAdj.HomEquiv.toRestriction_hom_apply, map_smulₛₗ,
-              RingHom.id_apply, CoextendScalars.smul_apply', one_mul] }
+        left_inv g := by ext; simp
+        right_inv g := by ext; simp }
     unit := RestrictionCoextensionAdj.unit'.{u₁, u₂, v} f
     counit := RestrictionCoextensionAdj.counit'.{u₁, u₂, v} f
     homEquiv_unit := hom_ext <| LinearMap.ext fun _ => rfl
-    homEquiv_counit := fun {X Y g} => by
+    homEquiv_counit {X Y g} := by
       ext
       simp [RestrictionCoextensionAdj.counit'] }
 
@@ -707,8 +702,6 @@ def HomEquiv.toRestrictScalars {X : ModuleCat R} {Y : ModuleCat S}
   { toFun := fun x => g <| (1 : S) ⊗ₜ[R,f] x
     map_add' := fun _ _ => by dsimp; rw [tmul_add, map_add]
     map_smul' := fun r s => by
-      letI : Module R S := Module.compHom S f
-      letI : Module R Y := Module.compHom Y f
       dsimp
       rw [RestrictScalars.smul_def, ← LinearMap.map_smul]
       erw [tmul_smul]

Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

@@ -113,7 +113,7 @@ theorem of_convergence_epsilon :
       _ ≤ fib n := by exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
       _ ≤ fib (n + 1) := by exact_mod_cast fib_le_fib_succ
       _ ≤ fib (n + 1) * fib (n + 1) := by exact_mod_cast (fib (n + 1)).le_mul_self
-      _ ≤ fib (n + 1) * fib (n + 2) := by gcongr; exact_mod_cast fib_le_fib_succ
+      _ ≤ fib (n + 1) * fib (n + 2) := by gcongr; lia
       _ ≤ B * nB := by gcongr
 
 theorem of_convergence [TopologicalSpace K] [OrderTopology K] :