Adaption for leanprover/lean4#6755

leanprover-community · Jan 27, 2025 · 5011e47 · 5011e47
1 parent 94c6906
commit 5011e47
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 6 deletions.
diff --git a/Mathlib/Algebra/LinearRecurrence.lean b/Mathlib/Algebra/LinearRecurrence.lean
@@ -92,11 +92,12 @@ theorem eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : Fin E.order → α}
   rw [mkSol]
   split_ifs with h'
   · exact mod_cast heq ⟨n, h'⟩
-  rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
-  congr with k
-  have : n - E.order + k < n := by omega
-  rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]
-  simp
+  · dsimp only
+    rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
+    congr with k
+    have : n - E.order + k < n := by omega
+    rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]
+    simp
 
 /-- If `u` is a solution to `E` and `init` designates its first `E.order` values,
   then `u = E.mkSol init`. This proves that `E.mkSol init` is the only solution

diff --git a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
@@ -575,7 +575,8 @@ private def fastJacobiSym (a : ℤ) (b : ℕ) : ℤ :=
     refine Nat.le_of_dvd (Int.gcd_pos_iff.mpr (mod_cast .inr hb0)) ?_
     refine Nat.dvd_gcd (Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero ha2)) ?_
     exact Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero (mod_cast hb2))
-  · rw [← IH (b / 2) (b.div_lt_self (Nat.pos_of_ne_zero hb0) one_lt_two)]
+  · dsimp only
+    rw [← IH (b / 2) (b.div_lt_self (Nat.pos_of_ne_zero hb0) one_lt_two)]
     obtain ⟨b, rfl⟩ := Nat.dvd_of_mod_eq_zero hb2
     rw [mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h),
       b.mul_div_cancel_left (by decide), mod_left a 2, Nat.cast_ofNat,