[Merged by Bors] - feat(Tactic): automatically replace convert with convert!

Archive/Examples/Eisenstein.lean

@@ -59,7 +59,7 @@ example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
       CharP.ker_intAlgebraMap_eq_span 3, span_singleton_pow, mem_span_singleton]
       norm_num
     rw [hfq, ← modByMonicHom_apply, map_add]
-    convert zero_add _
+    convert! zero_add _
     · rw [← LinearMap.mem_ker, mem_ker_modByMonic hq_monic]
       rw [pow_two, ← sub_mul]
       apply dvd_mul_left

Archive/Imo/Imo1959Q2.lean

@@ -60,7 +60,7 @@ theorem sqrt_two_mul_sub_one_le_one : sqrt (2 * x - 1) ≤ 1 ↔ x ≤ 1 := by
 theorem isGood_iff_eq_sqrt_two (hx : x ∈ Icc (1 / 2) 1) : IsGood x A ↔ A = sqrt 2 := by
   have : sqrt (2 * x - 1) ≤ 1 := sqrt_two_mul_sub_one_le_one.2 hx.2
   simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
-  suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this using 2; ring
+  suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert! this using 2; ring
   rw [← div_eq_iff, div_sqrt, eq_comm]
   positivity
 

Archive/Imo/Imo1982Q3.lean

@@ -74,7 +74,7 @@ end Imo1982Q3
 theorem imo1982_q3a (hx : Antitone x) (h0 : x 0 = 1) (hp : ∀ k, 0 < x k) :
     ∃ n : ℕ, 3.999 ≤ ∑ k ∈ range n, (x k) ^ 2 / x (k + 1) := by
   use 4000
-  convert Imo1982Q3.ineq (Nat.succ_ne_zero 3998) hx h0 hp
+  convert! Imo1982Q3.ineq (Nat.succ_ne_zero 3998) hx h0 hp
   norm_num
 
 /-- Part b of the problem is solved by `x k = (1 / 2) ^ k`. -/
@@ -88,6 +88,6 @@ theorem imo1982_q3b : ∃ x : ℕ → ℝ, Antitone x ∧ x 0 = 1 ∧ (∀ k, 0
     simp_rw [← pow_mul, pow_succ, ← div_eq_mul_inv, div_div_eq_mul_div, mul_comm, mul_div_assoc,
       ← mul_sum, div_eq_mul_inv, this, ← two_add_two_eq_four, ← mul_two,
       mul_lt_mul_iff_of_pos_left two_pos]
-    convert NNReal.coe_lt_coe.2 <| geom_sum_lt (inv_ne_zero two_ne_zero) two_inv_lt_one n
+    convert! NNReal.coe_lt_coe.2 <| geom_sum_lt (inv_ne_zero two_ne_zero) two_inv_lt_one n
     · simp
     · norm_num

Archive/Imo/Imo1994Q1.lean

@@ -54,7 +54,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
   -- `i ↦ m-i`
   -- We reindex the sum by fin (m+1)
   have : ∑ x ∈ A, x = ∑ i : Fin (m + 1), a i := by
-    convert sum_image fun x _ y _ => a.eq_iff_eq.1
+    convert! sum_image fun x _ y _ => a.eq_iff_eq.1
     rw [← coe_inj]; simp [a]
   rw [this]; clear this
   -- The main proof is a simple calculation by rearranging one of the two sums

Archive/Imo/Imo1998Q2.lean

@@ -210,7 +210,7 @@ end
 theorem clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
     (b - 1 : ℚ) / (2 * b) ≤ k / a ↔ ((b : ℕ) - 1) * a ≤ k * (2 * b) := by
   rw [div_le_div_iff₀]
-  on_goal 1 => convert Nat.cast_le (α := ℚ)
+  on_goal 1 => convert! Nat.cast_le (α := ℚ)
   all_goals simp [ha, hb]
 
 end

Archive/Imo/Imo2001Q5.lean

@@ -104,7 +104,7 @@ lemma x_pos : 0 < s.x := by
   have col := s.ABC_eq; rw [h, mul_zero] at col
   replace col : Collinear ℝ {s.A, s.B, s.C} := by
     apply collinear_of_sin_eq_zero; rw [col, Real.sin_zero]
-  apply s.not_collinear_BAC; convert col using 1; grind
+  apply s.not_collinear_BAC; convert! col using 1; grind
 
 lemma Q_ne_A : s.Q ≠ s.A := by
   by_contra h; have := s.ABQ_eq
@@ -127,7 +127,7 @@ lemma x_lt_pi_div_three : s.x < π / 3 := by
   have col : ∠ s.A s.C s.B = 0 := by linarith [s.ACB_eq, angle_nonneg s.A s.C s.B]
   replace col : Collinear ℝ {s.A, s.C, s.B} := by
     apply collinear_of_sin_eq_zero; rw [col, Real.sin_zero]
-  apply s.not_collinear_BAC; convert col using 1; grind
+  apply s.not_collinear_BAC; convert! col using 1; grind
 
 lemma APB_eq : ∠ s.A s.P s.B = 5 * π / 6 - 2 * s.x := by
   have := angle_add_angle_add_angle_eq_pi s.P s.A_ne_B

Archive/Imo/Imo2006Q3.lean

@@ -79,8 +79,8 @@ theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
   · rw [div_mul_eq_mul_div, le_div_iff₀' zero_lt_32]
     exact subst_wlog h' hxyz
   rcases (mul_nonneg_of_three x y z).resolve_left h' with h | h
-  · convert this y z x _ h using 2 <;> linarith
-  · convert this z x y _ h using 2 <;> linarith
+  · convert! this y z x _ h using 2 <;> linarith
+  · convert! this z x y _ h using 2 <;> linarith
 
 theorem proof₁ {a b c : ℝ} :
     |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤

Archive/Imo/Imo2006Q5.lean

@@ -72,7 +72,7 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
   have Hdvd : C.Chain (· ∣ ·) := by
     rw [Cycle.chain_map, periodicOrbit_chain' _ ht]
     intro n
-    convert sub_dvd_eval_sub ((fun x => P.eval x)^[n + 1] t) ((fun x => P.eval x)^[n] t) P <;>
+    convert! sub_dvd_eval_sub ((fun x => P.eval x)^[n + 1] t) ((fun x => P.eval x)^[n] t) P <;>
       rw [Function.iterate_succ_apply']
   -- Any two entries in C have the same absolute value.
   have Habs :
@@ -112,7 +112,7 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
     -- They must have opposite sign, so that P^{k + 1}(t) - P^k(t) = P^{k + 2}(t) - P^{k + 1}(t).
     rcases Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' | hn'
     · apply (hn _).elim
-      convert hn' <;> simp only [Function.iterate_succ_apply']
+      convert! hn' <;> simp only [Function.iterate_succ_apply']
     -- We deduce P^{k + 2}(t) = P^k(t) and hence P(P(t)) = t.
     · rw [neg_sub, sub_right_inj] at hn'
       simp only [Function.iterate_succ_apply'] at hn'

Archive/Imo/Imo2008Q2.lean

@@ -51,7 +51,7 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠
   have hmn_ne_zero : m + n ≠ 0 := by contrapose hz; field_simp; linarith
   have hc_sub_sub : c - (c - m - n) = m + n := by abel
   rw [ge_iff_le, ← sub_nonneg]
-  convert sq_nonneg ((c * (m ^ 2 + n ^ 2 + m * n) - m * (m + n) ^ 2) / (m * n * (m + n)))
+  convert! sq_nonneg ((c * (m ^ 2 + n ^ 2 + m * n) - m * (m + n) ^ 2) / (m * n * (m + n)))
   simp [field, hc_sub_sub]; ring
 
 def rationalSolutions :=

Archive/Imo/Imo2010Q5.lean

@@ -79,7 +79,7 @@ lemma push {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 5) :
     Reachable (B - single i (B i) + single (i + 1) (2 * B i)) := by
   obtain hc | hc := (B i).eq_zero_or_pos
   · rwa [hc, mul_zero, single_zero, single_zero, add_zero, tsub_zero]
-  · convert (rB.move1 hi hc).push hi using 1
+  · convert! (rB.move1 hi hc).push hi using 1
     ext k; simp only [add_apply, sub_apply]
     rcases eq_or_ne k i with rfl | hk
     · simp_rw [single_eq_same, tsub_self, single_succ]
@@ -92,29 +92,29 @@ termination_by B i
 /-- `(0, 0, 5, 11, 0, 0)` is reachable. -/
 lemma five_eleven : Reachable (single 2 5 + single 3 11) := by
   have R : Reachable (single 1 3 + single 2 1 + single 3 1 + single 4 1 + single 5 1) := by
-    convert base.push (show 0 < 5 by decide) using 1; decide
+    convert! base.push (show 0 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 7 + single 3 1 + single 4 1 + single 5 1) := by
-    convert R.push (show 1 < 5 by decide) using 1; decide
+    convert! R.push (show 1 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 7 + single 4 3 + single 5 1) := by
-    convert R.push (show 3 < 5 by decide) using 1; decide
+    convert! R.push (show 3 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 7 + single 5 7) := by
-    convert R.push (show 4 < 5 by decide) using 1; decide
+    convert! R.push (show 4 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 3 2 + single 5 7) := by
-    convert R.move1 (show 2 < 5 by decide) (by decide) using 1; decide
+    convert! R.move1 (show 2 < 5 by decide) (by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 3 1 + single 4 2 + single 5 7) := by
-    convert R.move1 (show 3 < 5 by decide) (by decide) using 1; decide
+    convert! R.move1 (show 3 < 5 by decide) (by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 3 1 + single 5 11) := by
-    convert R.push (show 4 < 5 by decide) using 1; decide
+    convert! R.push (show 4 < 5 by decide) using 1; decide
   replace R : Reachable (single 2 6 + single 4 11) := by
-    convert R.move2 (show 3 < 4 by decide) (by decide) using 1; decide
-  convert R.move2 (show 2 < 4 by decide) (by decide) using 1; decide
+    convert! R.move2 (show 3 < 4 by decide) (by decide) using 1; decide
+  convert! R.move2 (show 2 < 4 by decide) (by decide) using 1; decide
 
 /-- Decrement $B_i$ and double $B_{i+1}$, assuming $B_{i+2} = 0$, by doing `push, move2`. -/
 lemma double {B : Fin 6 → ℕ} {i : Fin 6}
     (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 2) = 0) :
     Reachable (B + single (i + 1) (B (i + 1)) - single i 1) := by
-  convert (rB.push (show i + 1 < 5 by grind)).move2 hi (by
-    rw [add_apply, sub_apply, single_succ]; grind)
+  convert!
+    (rB.push (show i + 1 < 5 by grind)).move2 hi (by rw [add_apply, sub_apply, single_succ]; grind)
   ext k; simp only [comp_apply, add_apply, sub_apply]
   have (j : Fin 6) : j + 1 + 1 = j + 2 := by grind
   rcases eq_or_ne k i with rfl | hk
@@ -132,7 +132,7 @@ lemma doubles {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (z
     Reachable (update (B - single i (B i)) (i + 1) (B (i + 1) * 2 ^ B i)) := by
   obtain hc | hc := (B i).eq_zero_or_pos
   · rwa [hc, single_zero, tsub_zero, pow_zero, mul_one, update_eq_self]
-  · convert (rB.double hi hc zB).doubles hi (by
+  · convert! (rB.double hi hc zB).doubles hi (by
       rw [sub_apply, add_apply, single_eq_of_ne (by simp), zB, zero_add, zero_tsub]) using 1
     ext k
     simp_rw [sub_apply, add_apply, single_eq_same, single_succ, single_succ', add_zero, tsub_zero,
@@ -149,9 +149,9 @@ termination_by B i
 lemma exp {B : Fin 6 → ℕ} {i : Fin 6}
     (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 1) = 0) (zB' : B (i + 2) = 0) :
     Reachable (B - single i (B i) + single (i + 1) (2 ^ B i)) := by
-  convert (rB.move1 (show i < 5 by grind) pB).doubles hi (by
+  convert! (rB.move1 (show i < 5 by grind) pB).doubles hi (by
     rw [add_apply, sub_apply, zB', single_eq_of_ne (by simp), tsub_zero,
-      single_eq_of_ne (by simp), zero_add]) using 1
+        single_eq_of_ne (by simp), zero_add]) using 1
   simp_rw [add_apply, sub_apply, single_eq_same, single_succ, single_succ', zB, zero_tsub, zero_add,
     add_zero, ← pow_succ', Nat.sub_add_cancel pB]
   ext k; simp only [add_apply, sub_apply]
@@ -167,7 +167,7 @@ lemma exp_mid {k n : ℕ} (h : Reachable (single 2 (k + 1) + single 3 n)) (hn :
     Reachable (single 2 k + single 3 (2 ^ n)) := by
   have md := h.exp (show 3 < 4 by decide) (by simp [hn])
     (by simp [add_apply, single_eq_of_ne]) (by simp [add_apply, single_eq_of_ne])
-  convert md.move2 (show 2 < 4 by decide) (by
+  convert! md.move2 (show 2 < 4 by decide) (by
     simp only [add_apply, sub_apply, single_eq_same]
     iterate 3 rw [single_eq_of_ne (by decide)]
     simp) using 1
@@ -192,7 +192,7 @@ lemma reduce {m n : ℕ} (h : Reachable (single 3 n)) (hmn : m ≤ n) : Reachabl
   | base => exact h
   | succ k _ ih =>
     apply ih
-    convert h.move2 (show 3 < 4 by decide) k.succ_pos
+    convert! h.move2 (show 3 < 4 by decide) k.succ_pos
     ext i; simp only [sub_apply, comp_apply]
     rcases eq_or_ne i 3 with rfl | i3
     · rw [swap_apply_of_ne_of_ne (by decide) (by decide)]
@@ -231,7 +231,7 @@ theorem result : Reachable (single 5 (2010 ^ 2010 ^ 2010)) := by
   -- See https://github.com/leanprover/lean4/issues/11713
   set m : ℕ := 2010
   have hm : m = 2010 := by rfl
-  convert ((quarter_target hm).push (show 3 < 5 by decide)).push (show 4 < 5 by decide)
+  convert! ((quarter_target hm).push (show 3 < 5 by decide)).push (show 4 < 5 by decide)
   simp only [single_eq_same, tsub_self, Fin.reduceAdd, zero_add, single_inj]
   rw [← mul_assoc, show 2 * 2 = 4 by rfl, mul_comm, Nat.div_mul_cancel]
   trans 2010 ^ 2

Archive/Imo/Imo2015Q6.lean

@@ -161,15 +161,15 @@ lemma sum_telescope {m n : ℕ} (hm : N ≤ m) (hn : m < n) :
 
 include ht in
 lemma le_sum_pool : ∑ i ∈ range b, (i : ℤ) ≤ ∑ x ∈ pool a t, x := by
-  convert sum_range_le_sum fun x mx ↦ (mem_Icc.mp ((pool_subset_Icc ha) mx)).1
+  convert! sum_range_le_sum fun x mx ↦ (mem_Icc.mp ((pool_subset_Icc ha) mx)).1
   · rw [hbN _ ht]
   · rw [zero_add]
 
 include ht in
 lemma sum_pool_le : ∑ x ∈ pool a t, x ≤ ∑ i ∈ range (b - 1), (2014 - i : ℤ) := by
   have zmp := zero_mem_pool ha hbN ht
   rw [← insert_erase zmp, sum_insert (notMem_erase _ _), zero_add]
-  convert sum_le_sum_range fun x mx ↦ ?_
+  convert! sum_le_sum_range fun x mx ↦ ?_
   · rw [card_erase_of_mem zmp, hbN _ ht]
   · exact (mem_Icc.mp ((pool_subset_Icc ha) (mem_erase.mp mx).2)).2
 

Archive/Imo/Imo2019Q2.lean

@@ -309,7 +309,7 @@ theorem sbtw_A_B₁_C : Sbtw ℝ cfg.A cfg.B₁ cfg.C :=
 
 theorem sbtw_A_A₁_A₂ : Sbtw ℝ cfg.A cfg.A₁ cfg.A₂ := by
   refine Sphere.sbtw_secondInter cfg.A_mem_circumsphere ?_
-  convert cfg.sbtw_B_A₁_C.dist_lt_max_dist _
+  convert! cfg.sbtw_B_A₁_C.dist_lt_max_dist _
   change _ = max (dist (cfg.triangleABC.points 1) _) (dist (cfg.triangleABC.points 2) _)
   simp_rw [circumsphere_center, circumsphere_radius, dist_circumcenter_eq_circumradius, max_self]
 
@@ -375,7 +375,7 @@ variable [Module.Oriented ℝ V (Fin 2)]
 theorem two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂ :
     (2 : ℤ) • ∡ cfg.Q cfg.P cfg.A₂ = (2 : ℤ) • ∡ cfg.B cfg.A cfg.A₂ := by
   refine two_zsmul_oangle_of_parallel cfg.QP_parallel_BA ?_
-  convert AffineSubspace.Parallel.refl (k := ℝ) (P := Pt) _ using 1
+  convert! AffineSubspace.Parallel.refl (k := ℝ) (P := Pt) _ using 1
   rw [cfg.collinear_PAA₁A₂.affineSpan_eq_of_ne (Set.mem_insert_of_mem _
     (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))
     (Set.mem_insert_of_mem _ (Set.mem_insert _ _)) cfg.A₂_ne_A,

Archive/Imo/Imo2024Q1.lean

@@ -52,7 +52,7 @@ lemma condition_sub_two_mul_int_iff {α : ℝ} (m : ℤ) : Condition (α - 2 * m
   simp_rw [← Finset.sum_sub_distrib, mul_sub]
   norm_cast
   simp_rw [Int.floor_sub_intCast, sub_sub_cancel_left]
-  convert condition_two_mul_int (-m) n hn
+  convert! condition_two_mul_int (-m) n hn
   norm_cast
   rw [Int.floor_intCast]
   simp
@@ -76,9 +76,9 @@ lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
   apply hr.ne'
   suffices ⌈α⁻¹⌉₊ = (1 : ℤ) from mod_cast this
   apply Int.eq_one_of_dvd_one (Int.zero_le_ofNat _)
-  convert hc ⌈α⁻¹⌉₊ (zero_lt_one.trans hr)
+  convert! hc ⌈α⁻¹⌉₊ (zero_lt_one.trans hr)
   rw [← Finset.add_sum_Ico_eq_sum_Icc hr.le]
-  convert (add_zero _).symm
+  convert! (add_zero _).symm
   · rw [Int.floor_eq_iff]
     constructor
     · rw [Int.cast_one]
@@ -129,7 +129,7 @@ lemma mem_Ico_n_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) {n : ℕ} (hn : 0 < n) :
       by_contra
       rw [show ⌊(k + 1 : ℕ) * α⌋ = 2 * k by lia] at hc
       have hc' : ((k + 1 : ℕ) : ℤ) ∣ ((k + 1 : ℕ) : ℤ) * ((k + 1 : ℕ) : ℤ) - 1 := by
-        convert hc using 1
+        convert! hc using 1
         push_cast
         ring
       rw [dvd_sub_right (dvd_mul_right _ _), ← isUnit_iff_dvd_one, Int.isUnit_iff] at hc'
@@ -140,7 +140,7 @@ lemma mem_Ico_n_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) {n : ℕ} (hn : 0 < n) :
       ring
     · rw [Int.floor_eq_iff] at hk'
       rw [div_le_iff₀ (by norm_cast; lia), mul_comm α]
-      convert hk'.1
+      convert! hk'.1
       push_cast
       ring
 
@@ -153,7 +153,7 @@ lemma not_condition_of_mem_Ioo {α : ℝ} (h : α ∈ Set.Ioo 0 2) : ¬Condition
   have hna := (hc.mem_Ico_n_of_mem_Ioo h hn).1
   rcases h with ⟨-, h2⟩
   have hna' : 2 - (n : ℝ)⁻¹ ≤ α := by
-    convert hna using 1
+    convert! hna using 1
     field
   rw [sub_eq_add_neg, ← le_sub_iff_add_le', neg_le, neg_sub] at hna'
   rw [le_inv_comm₀ (by linarith) (mod_cast hn), ← not_lt] at hna'
@@ -167,7 +167,7 @@ lemma condition_iff_of_mem_Ico {α : ℝ} (h : α ∈ Set.Ico 0 2) : Condition 
     | inl h => exact h
     | inr ho => exact False.elim (not_condition_of_mem_Ioo ho hc)
   · rintro rfl
-    convert condition_two_mul_int 0
+    convert! condition_two_mul_int 0
     norm_num
 
 recall Imo2024Q1.Condition (α : ℝ) := (∀ n : ℕ, 0 < n → (n : ℤ) ∣ ∑ i ∈ Finset.Icc 1 n, ⌊i * α⌋)

Archive/Imo/Imo2024Q2.lean

@@ -32,12 +32,12 @@ lemma dvd_pow_iff_of_dvd_sub {a b d n : ℕ} {z : ℤ} (ha : a.Coprime d)
     d ∣ a ^ n + b ↔ (((ZMod.unitOfCoprime _ ha) ^ z : (ZMod d)ˣ) : ZMod d) + b = 0 := by
   rcases hd with ⟨k, hk⟩
   rw [← ZMod.natCast_eq_zero_iff]
-  convert Iff.rfl
+  convert! Iff.rfl
   push_cast
   congr
   suffices (((ZMod.unitOfCoprime _ ha) ^ z : (ZMod d)ˣ) : ZMod d) =
       (((ZMod.unitOfCoprime _ ha) ^ (n : ℤ) : (ZMod d)ˣ) : ZMod d) by
-    convert this
+    convert! this
   rw [sub_eq_iff_eq_add] at hk
   rw [hk, zpow_add, zpow_mul]
   norm_cast
@@ -139,11 +139,11 @@ lemma ab_add_one_dvd_a_pow_large_n_add_b : a * b + 1 ∣ a ^ h.large_n + b := by
   norm_cast
   simp only [mul_inv_cancel, Units.val_one, ZMod.coe_unitOfCoprime]
   norm_cast
-  convert ZMod.natCast_self (a * b + 1) using 2
+  convert! ZMod.natCast_self (a * b + 1) using 2
   exact add_comm _ _
 
 lemma ab_add_one_dvd_b_pow_large_n_add_a : a * b + 1 ∣ b ^ h.large_n + a := by
-  convert h.symm.ab_add_one_dvd_a_pow_large_n_add_b using 1
+  convert! h.symm.ab_add_one_dvd_a_pow_large_n_add_b using 1
   · rw [mul_comm]
   · rw [h.symm_large_n]