bump to nightly-2023-12-20-06

mathlib commit leanprover-community/mathlib@65a1391

Archive/Imo/Imo2001Q2.lean

@@ -51,7 +51,7 @@ theorem bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
   rw [div_le_div_iff hdenom (sqrt_pos.mpr hsqrt)]
   conv_lhs => rw [pow_succ', mul_assoc]
   apply mul_le_mul_of_nonneg_left _ (pow_pos ha 3).le
-  apply le_of_pow_le_pow _ hdenom.le zero_lt_two
+  apply le_of_pow_le_pow_left _ hdenom.le zero_lt_two
   rw [mul_pow, sq_sqrt hsqrt.le, ← sub_nonneg]
   calc
     (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) =

Archive/Imo/Imo2006Q3.lean

@@ -84,9 +84,9 @@ theorem subst_wlog {x y z s : ℝ} (hxy : 0 ≤ x * y) (hxyz : x + y + z = 0) :
         le_trans (mul_le_mul_of_nonneg_left (lhs_ineq hxy) hs) mid_ineq
       _ ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4 :=
         div_le_div_of_le four_pow_four_pos.le <|
-          pow_le_pow_of_le_left (add_nonneg (mul_nonneg zero_lt_three.le (sq_nonneg _)) hs)
+          pow_le_pow_left (add_nonneg (mul_nonneg zero_lt_three.le (sq_nonneg _)) hs)
             (add_le_add_right rhs_ineq _) _
-  le_of_pow_le_pow _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) Nat.succ_pos' <|
+  le_of_pow_le_pow_left _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) Nat.succ_pos' <|
     calc
       (32 * |x * y * z * s|) ^ 2 = 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2)) := by
         rw [mul_pow, sq_abs, hz] <;> ring

Archive/Imo/Imo2008Q3.lean

@@ -67,11 +67,11 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   have hreal₃ : (k : ℝ) ^ 2 + 4 ≥ p := by assumption_mod_cast
   have hreal₅ : (k : ℝ) > 4 :=
     by
-    refine' lt_of_pow_lt_pow 2 k.cast_nonneg _
+    refine' lt_of_pow_lt_pow_left 2 k.cast_nonneg _
     linarith only [hreal₂, hreal₃]
   have hreal₆ : (k : ℝ) > sqrt (2 * n) :=
     by
-    refine' lt_of_pow_lt_pow 2 k.cast_nonneg _
+    refine' lt_of_pow_lt_pow_left 2 k.cast_nonneg _
     rw [sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg)]
     linarith only [hreal₁, hreal₃, hreal₅]
   exact ⟨n, hnat₁, by linarith only [hreal₆, hreal₁]⟩

Archive/Imo/Imo2013Q1.lean

@@ -38,7 +38,7 @@ theorem arith_lemma (k n : ℕ) : 0 < 2 * n + 2 ^ k.succ :=
   calc
     0 < 2 := zero_lt_two
     _ = 2 ^ 1 := (pow_one 2).symm
-    _ ≤ 2 ^ k.succ := (Nat.pow_le_pow_of_le_right zero_lt_two (Nat.le_add_left 1 k))
+    _ ≤ 2 ^ k.succ := (Nat.pow_le_pow_right zero_lt_two (Nat.le_add_left 1 k))
     _ ≤ 2 * n + 2 ^ k.succ := Nat.le_add_left _ _
 #align imo2013_q1.arith_lemma Imo2013Q1.arith_lemma
 

Archive/Imo/Imo2013Q5.lean

@@ -98,7 +98,7 @@ theorem le_of_all_pow_lt_succ' {x y : ℝ} (hx : 1 < x) (hy : 0 < y)
     intro n hn
     calc
       x ^ n - 1 < y ^ n := h n hn
-      _ ≤ y' ^ n := pow_le_pow_of_le_left hy.le h_y_lt_y'.le n
+      _ ≤ y' ^ n := pow_le_pow_left hy.le h_y_lt_y'.le n
   exact h_y'_lt_x.not_le (le_of_all_pow_lt_succ hx h1_lt_y' hh)
 #align imo2013_q5.le_of_all_pow_lt_succ' Imo2013Q5.le_of_all_pow_lt_succ'
 

Archive/Imo/Imo2019Q4.lean

@@ -56,7 +56,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0) (h : (k ! : ℤ) = ∏ i in range n
   suffices (∏ i in range n, 2 ^ n : ℤ) < ↑k !
     by
     apply lt_of_le_of_lt _ this; apply prod_le_prod
-    · intros; rw [sub_nonneg]; apply pow_le_pow; norm_num; apply le_of_lt; rwa [← mem_range]
+    · intros; rw [sub_nonneg]; apply pow_le_pow_right; norm_num; apply le_of_lt; rwa [← mem_range]
     · intros; apply sub_le_self; apply pow_nonneg; norm_num
   suffices 2 ^ (n * n) < (n * (n - 1) / 2)!
     by
@@ -76,7 +76,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0) (h : (k ! : ℤ) = ∏ i in range n
   rw [triangle_succ]; apply lt_of_lt_of_le _ factorial_mul_pow_le_factorial
   refine'
     lt_of_le_of_lt _
-      (mul_lt_mul ih (Nat.pow_le_pow_of_le_left this _) (pow_pos (by norm_num) _) (zero_le _))
+      (mul_lt_mul ih (Nat.pow_le_pow_left this _) (pow_pos (by norm_num) _) (zero_le _))
   rw [← pow_mul, ← pow_add]; apply pow_le_pow_of_le_right; norm_num
   rw [add_mul 2 2]
   convert add_le_add_left (add_le_add_left h5 (2 * n')) (n' * n') using 1; ring

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -131,7 +131,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
   · have hf1 : f 1 < 0 := by norm_num [hf, hb]
     have hfa : 0 ≤ f a := by
       simp_rw [hf, ← sq]
-      refine' add_nonneg (sub_nonneg.mpr (pow_le_pow ha _)) _ <;> norm_num
+      refine' add_nonneg (sub_nonneg.mpr (pow_le_pow_right ha _)) _ <;> norm_num
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (set.mem_Ioc.mpr ⟨hf1, hf0⟩)
     obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (set.mem_Ioc.mpr ⟨hf1, hfa⟩)
     exact ⟨x, y, (hx1.trans hy1).Ne, hx2, hy2⟩
@@ -141,7 +141,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
       calc
         f (-a) = a ^ 2 - a ^ 5 + b := by norm_num [hf, ← sq]
         _ ≤ a ^ 2 - a ^ 3 + (a - 1) := by
-          refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith
+          refine' add_le_add (sub_le_sub_left (pow_le_pow_right ha _) _) _ <;> linarith
         _ = -(a - 1) ^ 2 * (a + 1) := by ring
         _ ≤ 0 := by nlinarith
     have ha' := neg_nonpos.mpr (hle.trans ha)

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -170,7 +170,7 @@ theorem card_le_two_pow {x k : ℕ} : card ({e ∈ m x k | Squarefree (e + 1)})
     card M₁ ≤ card (image f K) := card_le_of_subset h
     _ ≤ card K := card_image_le
     _ ≤ 2 ^ card (image Nat.succ (range k)) := by simp only [K, card_powerset]
-    _ ≤ 2 ^ card (range k) := (pow_le_pow one_le_two card_image_le)
+    _ ≤ 2 ^ card (range k) := (pow_le_pow_right one_le_two card_image_le)
     _ = 2 ^ k := by rw [card_range k]
 #align theorems_100.card_le_two_pow Theorems100.card_le_two_pow
 

Mathbin/Algebra/Category/Algebra/Basic.lean

@@ -150,7 +150,7 @@ def free : Type u ⥤ AlgebraCat.{u} R
       isRing := Algebra.semiringToRing R }
   map S T f := FreeAlgebra.lift _ <| FreeAlgebra.ι _ ∘ f
   -- obviously can fill the next two goals, but it is slow
-  map_id' := by intro X; ext1; simp only [FreeAlgebra.ι_comp_lift]; rfl
+  map_id'' := by intro X; ext1; simp only [FreeAlgebra.ι_comp_lift]; rfl
   map_comp' := by
     intros; ext1; simp only [FreeAlgebra.ι_comp_lift]; ext1
     simp only [FreeAlgebra.lift_ι_apply, CategoryTheory.coe_comp, Function.comp_apply,

Mathbin/Algebra/Category/Module/FilteredColimits.lean

@@ -94,16 +94,16 @@ theorem colimitSMulAux_eq_of_rel (r : R) (x y : Σ j, F.obj j)
 #align Module.filtered_colimits.colimit_smul_aux_eq_of_rel ModuleCat.FilteredColimits.colimitSMulAux_eq_of_rel
 -/
 
-#print ModuleCat.FilteredColimits.colimitHasSmul /-
+#print ModuleCat.FilteredColimits.colimitHasSMul /-
 /-- Scalar multiplication in the colimit. See also `colimit_smul_aux`. -/
-instance colimitHasSmul : SMul R M
+instance colimitHasSMul : SMul R M
     where smul r x := by
     refine' Quot.lift (colimit_smul_aux F r) _ x
     intro x y h
     apply colimit_smul_aux_eq_of_rel
     apply types.filtered_colimit.rel_of_quot_rel
     exact h
-#align Module.filtered_colimits.colimit_has_smul ModuleCat.FilteredColimits.colimitHasSmul
+#align Module.filtered_colimits.colimit_has_smul ModuleCat.FilteredColimits.colimitHasSMul
 -/
 
 #print ModuleCat.FilteredColimits.colimit_smul_mk_eq /-

Mathbin/Algebra/FreeAlgebra.lean

@@ -116,13 +116,13 @@ def hasOne : One (Pre R X) :=
 #align free_algebra.pre.has_one FreeAlgebra.Pre.hasOne
 -/
 
-#print FreeAlgebra.Pre.hasSmul /-
+#print FreeAlgebra.Pre.hasSMul /-
 /-- Scalar multiplication defined as multiplication by the image of elements from `R`.
 Note: Used for notation only.
 -/
-def hasSmul : SMul R (Pre R X) :=
+def hasSMul : SMul R (Pre R X) :=
   ⟨fun r m => mul (ofScalar r) m⟩
-#align free_algebra.pre.has_smul FreeAlgebra.Pre.hasSmul
+#align free_algebra.pre.has_smul FreeAlgebra.Pre.hasSMul
 -/
 
 end Pre

Mathbin/Algebra/GeomSum.lean

@@ -239,9 +239,9 @@ theorem sub_dvd_pow_sub_pow [CommRing α] (x y : α) (n : ℕ) : x - y ∣ x ^ n
 theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n :=
   by
   cases' le_or_lt y x with h
-  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _
+  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
     exact_mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
-  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_of_le_left h.le _
+  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
     exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)
 #align nat_sub_dvd_pow_sub_pow nat_sub_dvd_pow_sub_pow
 -/

Mathbin/Algebra/GradedMulAction.lean

@@ -63,39 +63,39 @@ variable (A : ι → Type _) (M : ι → Type _)
 
 /-- A graded version of `has_smul`. Scalar multiplication combines grades additively, i.e.
 if `a ∈ A i` and `m ∈ M j`, then `a • b` must be in `M (i + j)`-/
-class GSmul [Add ι] where
+class GSMul [Add ι] where
   smul {i j} : A i → M j → M (i + j)
-#align graded_monoid.ghas_smul GradedMonoid.GSmulₓ
+#align graded_monoid.ghas_smul GradedMonoid.GSMulₓ
 
-#print GradedMonoid.GMul.toGSmul /-
+#print GradedMonoid.GMul.toGSMul /-
 /-- A graded version of `has_mul.to_has_smul` -/
-instance GMul.toGSmul [Add ι] [GMul A] : GSmul A A where smul _ _ := GMul.mul
-#align graded_monoid.ghas_mul.to_ghas_smul GradedMonoid.GMul.toGSmul
+instance GMul.toGSMul [Add ι] [GMul A] : GSMul A A where smul _ _ := GMul.mul
+#align graded_monoid.ghas_mul.to_ghas_smul GradedMonoid.GMul.toGSMul
 -/
 
-#print GradedMonoid.GSmul.toSMul /-
-instance GSmul.toSMul [Add ι] [GSmul A M] : SMul (GradedMonoid A) (GradedMonoid M) :=
-  ⟨fun (x : GradedMonoid A) (y : GradedMonoid M) => ⟨_, GSmul.smul x.snd y.snd⟩⟩
-#align graded_monoid.ghas_smul.to_has_smul GradedMonoid.GSmul.toSMul
+#print GradedMonoid.GSMul.toSMul /-
+instance GSMul.toSMul [Add ι] [GSMul A M] : SMul (GradedMonoid A) (GradedMonoid M) :=
+  ⟨fun (x : GradedMonoid A) (y : GradedMonoid M) => ⟨_, GSMul.smul x.snd y.snd⟩⟩
+#align graded_monoid.ghas_smul.to_has_smul GradedMonoid.GSMul.toSMul
 -/
 
 #print GradedMonoid.mk_smul_mk /-
-theorem mk_smul_mk [Add ι] [GSmul A M] {i j} (a : A i) (b : M j) :
-    mk i a • mk j b = mk (i + j) (GSmul.smul a b) :=
+theorem mk_smul_mk [Add ι] [GSMul A M] {i j} (a : A i) (b : M j) :
+    mk i a • mk j b = mk (i + j) (GSMul.smul a b) :=
   rfl
 #align graded_monoid.mk_smul_mk GradedMonoid.mk_smul_mk
 -/
 
 /-- A graded version of `mul_action`. -/
-class GMulAction [AddMonoid ι] [GMonoid A] extends GSmul A M where
+class GMulAction [AddMonoid ι] [GMonoid A] extends GSMul A M where
   one_smul (b : GradedMonoid M) : (1 : GradedMonoid A) • b = b
   hMul_smul (a a' : GradedMonoid A) (b : GradedMonoid M) : (a * a') • b = a • a' • b
 #align graded_monoid.gmul_action GradedMonoid.GMulActionₓ
 
 #print GradedMonoid.GMonoid.toGMulAction /-
 /-- The graded version of `monoid.to_mul_action`. -/
 instance GMonoid.toGMulAction [AddMonoid ι] [GMonoid A] : GMulAction A A :=
-  { GMul.toGSmul _ with
+  { GMul.toGSMul _ with
     one_smul := GMonoid.one_hMul
     hMul_smul := GMonoid.hMul_assoc }
 #align graded_monoid.gmonoid.to_gmul_action GradedMonoid.GMonoid.toGMulAction
@@ -122,34 +122,34 @@ section Subobjects
 variable {R : Type _}
 
 /-- A version of `graded_monoid.ghas_smul` for internally graded objects. -/
-class SetLike.GradedSmul {S R N M : Type _} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
+class SetLike.GradedSMul {S R N M : Type _} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
     (A : ι → S) (B : ι → N) : Prop where
   smul_mem : ∀ ⦃i j : ι⦄ {ai bj}, ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i + j)
-#align set_like.has_graded_smul SetLike.GradedSmulₓ
-
-#print SetLike.toGSmul /-
-instance SetLike.toGSmul {S R N M : Type _} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
-    (A : ι → S) (B : ι → N) [SetLike.GradedSmul A B] :
-    GradedMonoid.GSmul (fun i => A i) fun i => B i
-    where smul i j a b := ⟨(a : R) • b, SetLike.GradedSmul.smul_mem a.2 b.2⟩
-#align set_like.ghas_smul SetLike.toGSmul
+#align set_like.has_graded_smul SetLike.GradedSMulₓ
+
+#print SetLike.toGSMul /-
+instance SetLike.toGSMul {S R N M : Type _} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
+    (A : ι → S) (B : ι → N) [SetLike.GradedSMul A B] :
+    GradedMonoid.GSMul (fun i => A i) fun i => B i
+    where smul i j a b := ⟨(a : R) • b, SetLike.GradedSMul.smul_mem a.2 b.2⟩
+#align set_like.ghas_smul SetLike.toGSMul
 -/
 
-#print SetLike.coe_GSmul /-
+#print SetLike.coe_GSMul /-
 @[simp]
-theorem SetLike.coe_GSmul {S R N M : Type _} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
-    (A : ι → S) (B : ι → N) [SetLike.GradedSmul A B] {i j : ι} (x : A i) (y : B j) :
-    (@GradedMonoid.GSmul.smul ι (fun i => A i) (fun i => B i) _ _ i j x y : M) = (x : R) • y :=
+theorem SetLike.coe_GSMul {S R N M : Type _} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
+    (A : ι → S) (B : ι → N) [SetLike.GradedSMul A B] {i j : ι} (x : A i) (y : B j) :
+    (@GradedMonoid.GSMul.smul ι (fun i => A i) (fun i => B i) _ _ i j x y : M) = (x : R) • y :=
   rfl
-#align set_like.coe_ghas_smul SetLike.coe_GSmul
+#align set_like.coe_ghas_smul SetLike.coe_GSMul
 -/
 
-#print SetLike.GradedMul.toGradedSmul /-
+#print SetLike.GradedMul.toGradedSMul /-
 /-- Internally graded version of `has_mul.to_has_smul`. -/
-instance SetLike.GradedMul.toGradedSmul [AddMonoid ι] [Monoid R] {S : Type _} [SetLike S R]
-    (A : ι → S) [SetLike.GradedMonoid A] : SetLike.GradedSmul A A
+instance SetLike.GradedMul.toGradedSMul [AddMonoid ι] [Monoid R] {S : Type _} [SetLike S R]
+    (A : ι → S) [SetLike.GradedMonoid A] : SetLike.GradedSMul A A
     where smul_mem i j ai bj hi hj := SetLike.GradedMonoid.hMul_mem hi hj
-#align set_like.has_graded_mul.to_has_graded_smul SetLike.GradedMul.toGradedSmul
+#align set_like.has_graded_mul.to_has_graded_smul SetLike.GradedMul.toGradedSMul
 -/
 
 end Subobjects
@@ -160,9 +160,9 @@ variable {S R N M : Type _} [SetLike S R] [SetLike N M]
 
 #print SetLike.Homogeneous.graded_smul /-
 theorem SetLike.Homogeneous.graded_smul [Add ι] [SMul R M] {A : ι → S} {B : ι → N}
-    [SetLike.GradedSmul A B] {a : R} {b : M} :
+    [SetLike.GradedSMul A B] {a : R} {b : M} :
     SetLike.Homogeneous A a → SetLike.Homogeneous B b → SetLike.Homogeneous B (a • b)
-  | ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i + j, SetLike.GradedSmul.smul_mem hi hj⟩
+  | ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i + j, SetLike.GradedSMul.smul_mem hi hj⟩
 #align set_like.is_homogeneous.graded_smul SetLike.Homogeneous.graded_smul
 -/
 

Mathbin/Algebra/GroupPower/Lemmas.lean

@@ -378,14 +378,14 @@ theorem one_lt_zpow' (ha : 1 < a) {k : ℤ} (hk : (0 : ℤ) < k) : 1 < a ^ k :=
 #align zsmul_pos zsmul_pos
 -/
 
-#print zpow_strictMono_right /-
+#print zpow_right_strictMono /-
 @[to_additive zsmul_strictMono_left]
-theorem zpow_strictMono_right (ha : 1 < a) : StrictMono fun n : ℤ => a ^ n := fun m n h =>
+theorem zpow_right_strictMono (ha : 1 < a) : StrictMono fun n : ℤ => a ^ n := fun m n h =>
   calc
     a ^ m = a ^ m * 1 := (mul_one _).symm
     _ < a ^ m * a ^ (n - m) := (mul_lt_mul_left' (one_lt_zpow' ha <| sub_pos_of_lt h) _)
     _ = a ^ n := by rw [← zpow_add]; simp
-#align zpow_strict_mono_right zpow_strictMono_right
+#align zpow_strict_mono_right zpow_right_strictMono
 #align zsmul_strict_mono_left zsmul_strictMono_left
 -/
 
@@ -411,23 +411,23 @@ theorem zpow_le_zpow (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n :=
 #print zpow_lt_zpow /-
 @[to_additive]
 theorem zpow_lt_zpow (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
-  zpow_strictMono_right ha h
+  zpow_right_strictMono ha h
 #align zpow_lt_zpow zpow_lt_zpow
 #align zsmul_lt_zsmul zsmul_lt_zsmul
 -/
 
 #print zpow_le_zpow_iff /-
 @[to_additive]
 theorem zpow_le_zpow_iff (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
-  (zpow_strictMono_right ha).le_iff_le
+  (zpow_right_strictMono ha).le_iff_le
 #align zpow_le_zpow_iff zpow_le_zpow_iff
 #align zsmul_le_zsmul_iff zsmul_le_zsmul_iff
 -/
 
 #print zpow_lt_zpow_iff /-
 @[to_additive]
 theorem zpow_lt_zpow_iff (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
-  (zpow_strictMono_right ha).lt_iff_lt
+  (zpow_right_strictMono ha).lt_iff_lt
 #align zpow_lt_zpow_iff zpow_lt_zpow_iff
 #align zsmul_lt_zsmul_iff zsmul_lt_zsmul_iff
 -/
@@ -858,9 +858,9 @@ theorem strictMono_pow_bit1 (n : ℕ) : StrictMono fun a : R => a ^ bit1 n :=
   cases' le_total a 0 with ha ha
   · cases' le_or_lt b 0 with hb hb
     · rw [← neg_lt_neg_iff, ← neg_pow_bit1, ← neg_pow_bit1]
-      exact pow_lt_pow_of_lt_left (neg_lt_neg hab) (neg_nonneg.2 hb) (bit1_pos (zero_le n))
+      exact pow_lt_pow_left (neg_lt_neg hab) (neg_nonneg.2 hb) (bit1_pos (zero_le n))
     · exact (pow_bit1_nonpos_iff.2 ha).trans_lt (pow_bit1_pos_iff.2 hb)
-  · exact pow_lt_pow_of_lt_left hab ha (bit1_pos (zero_le n))
+  · exact pow_lt_pow_left hab ha (bit1_pos (zero_le n))
 #align strict_mono_pow_bit1 strictMono_pow_bit1
 -/