From 6c7d871c3833389330aff2e3d8556acbe25813ec Mon Sep 17 00:00:00 2001
From: e-271828 <f_s@har.bbiq.jp>
Date: Sat, 11 Apr 2026 14:06:13 +0900
Subject: [PATCH 1/5] feat(Analysis/Calculus/DSlope): add
 `eq_smul_dslope_of_zero` and iterated version

---
 Mathlib/Analysis/Calculus/DSlope.lean | 35 +++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/Mathlib/Analysis/Calculus/DSlope.lean b/Mathlib/Analysis/Calculus/DSlope.lean
index 7d1cf1104ae1fc..1060d293c75acd 100644
--- a/Mathlib/Analysis/Calculus/DSlope.lean
+++ b/Mathlib/Analysis/Calculus/DSlope.lean
@@ -141,3 +141,38 @@ theorem differentiableOn_dslope_of_notMem (h : a ∉ s) :
 theorem differentiableAt_dslope_of_ne (h : b ≠ a) :
     DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b := by
   simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- If `f a = 0`, then `f b = (b - a) • dslope f a b`. -/
+lemma eq_smul_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (hf : f a = 0) (b : 𝕜) :
+    f b = (b - a) • dslope f a b := by
+  by_cases h : b = a
+  · simp [h, hf]
+  · -- 正しく関数 f を渡して dslope を slope に展開する
+    rw [dslope_of_ne f h]
+    -- slope の定義（傾きの式）に強制的に書き換える
+    change f b = (b - a) • ((b - a)⁻¹ • (f b - f a))
+    -- (b - a) * (b - a)⁻¹ = 1 となることを用いて代数的に約分する
+    rw [← mul_smul, mul_inv_cancel₀ (sub_ne_zero.mpr h)]
+    rw [one_smul, hf, sub_zero]
+
+/-- If `f` and its first `n-1` iterated dslopes at `a` vanish,
+then `f b = (b - a) ^ n • (Function.swap dslope a)^[n] f b`. -/
+lemma eq_pow_smul_iterate_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (n : ℕ)
+    (hf : ∀ k < n, (Function.swap dslope a)^[k] f a = 0) (b : 𝕜) :
+    f b = (b - a) ^ n • (Function.swap dslope a)^[n] f b := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    have h_lt : ∀ k < n, (Function.swap dslope a)^[k] f a = 0 :=
+      fun k hk => hf k (Nat.lt_trans hk (Nat.lt_succ_self n))
+    rw [ih h_lt]
+    have h_zero : (Function.swap dslope a)^[n] f a = 0 :=
+      hf n (Nat.lt_succ_self n)
+    have h_dslope := eq_smul_dslope_of_zero h_zero b
+    rw [h_dslope]
+    -- スカラー倍の結合法則と、累乗の定義を使って美しく整理する
+    rw [← mul_smul, ← pow_succ]
+    rw [Function.iterate_succ_apply']

From 252139db5ea237ca6c3f127d19aea72b069bb2f0 Mon Sep 17 00:00:00 2001
From: e-271828 <39018690+e-271828@users.noreply.github.com>
Date: Sat, 11 Apr 2026 23:47:58 +0900
Subject: [PATCH 2/5] Update Mathlib/Analysis/Calculus/DSlope.lean

Apply suggestion from wwylele to simplify proof using sub_smul_dslope

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
---
 Mathlib/Analysis/Calculus/DSlope.lean | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/DSlope.lean b/Mathlib/Analysis/Calculus/DSlope.lean
index 1060d293c75acd..4c427991a15380 100644
--- a/Mathlib/Analysis/Calculus/DSlope.lean
+++ b/Mathlib/Analysis/Calculus/DSlope.lean
@@ -148,15 +148,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 /-- If `f a = 0`, then `f b = (b - a) • dslope f a b`. -/
 lemma eq_smul_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (hf : f a = 0) (b : 𝕜) :
     f b = (b - a) • dslope f a b := by
-  by_cases h : b = a
-  · simp [h, hf]
-  · -- 正しく関数 f を渡して dslope を slope に展開する
-    rw [dslope_of_ne f h]
-    -- slope の定義（傾きの式）に強制的に書き換える
-    change f b = (b - a) • ((b - a)⁻¹ • (f b - f a))
-    -- (b - a) * (b - a)⁻¹ = 1 となることを用いて代数的に約分する
-    rw [← mul_smul, mul_inv_cancel₀ (sub_ne_zero.mpr h)]
-    rw [one_smul, hf, sub_zero]
+  simp [hf]
 
 /-- If `f` and its first `n-1` iterated dslopes at `a` vanish,
 then `f b = (b - a) ^ n • (Function.swap dslope a)^[n] f b`. -/

From 2f1e133d740aeae53b4a030fa821dfe57737f155 Mon Sep 17 00:00:00 2001
From: e-271828 <f_s@har.bbiq.jp>
Date: Thu, 16 Apr 2026 02:54:33 +0900
Subject: [PATCH 3/5] refactor: flip equalities and update proofs per reviewer
 suggestions

---
 Mathlib/Analysis/Calculus/DSlope.lean | 38 +++++++++++----------------
 1 file changed, 16 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/DSlope.lean b/Mathlib/Analysis/Calculus/DSlope.lean
index 4c427991a15380..d7ebfb7255838a 100644
--- a/Mathlib/Analysis/Calculus/DSlope.lean
+++ b/Mathlib/Analysis/Calculus/DSlope.lean
@@ -142,29 +142,23 @@ theorem differentiableAt_dslope_of_ne (h : b ≠ a) :
     DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b := by
   simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-
-/-- If `f a = 0`, then `f b = (b - a) • dslope f a b`. -/
-lemma eq_smul_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (hf : f a = 0) (b : 𝕜) :
-    f b = (b - a) • dslope f a b := by
-  simp [hf]
-
-/-- If `f` and its first `n-1` iterated dslopes at `a` vanish,
-then `f b = (b - a) ^ n • (Function.swap dslope a)^[n] f b`. -/
-lemma eq_pow_smul_iterate_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (n : ℕ)
+lemma sub_smul_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (hf : f a = 0) (b : 𝕜) :
+    (b - a) • dslope f a b = f b := by
+  by_cases h : b = a
+  · simp [h, hf]
+  · have h_dslope : dslope f a b = (b - a)⁻¹ • f b := by simp [dslope, slope, h, hf]
+    have h_sub_ne_zero : b - a ≠ 0 := sub_ne_zero.mpr h
+    rw [h_dslope, smul_smul]
+    simp [h_sub_ne_zero]
+
+lemma pow_sub_smul_iterate_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (n : ℕ)
     (hf : ∀ k < n, (Function.swap dslope a)^[k] f a = 0) (b : 𝕜) :
-    f b = (b - a) ^ n • (Function.swap dslope a)^[n] f b := by
-  induction n with
+    (b - a) ^ n • (Function.swap dslope a)^[n] f b = f b := by
+  induction n generalizing f with
   | zero => simp
   | succ n ih =>
-    have h_lt : ∀ k < n, (Function.swap dslope a)^[k] f a = 0 :=
+    rw [Function.iterate_succ_apply', pow_succ, mul_smul]
+    have hf_n : (Function.swap dslope a)^[n] f a = 0 := hf n (Nat.lt_succ_self n)
+    have hf_lt : ∀ k < n, (Function.swap dslope a)^[k] f a = 0 :=
       fun k hk => hf k (Nat.lt_trans hk (Nat.lt_succ_self n))
-    rw [ih h_lt]
-    have h_zero : (Function.swap dslope a)^[n] f a = 0 :=
-      hf n (Nat.lt_succ_self n)
-    have h_dslope := eq_smul_dslope_of_zero h_zero b
-    rw [h_dslope]
-    -- スカラー倍の結合法則と、累乗の定義を使って美しく整理する
-    rw [← mul_smul, ← pow_succ]
-    rw [Function.iterate_succ_apply']
+    rw [sub_smul_dslope_of_zero hf_n b, ih hf_lt]

From 6e7bcbbca587f4b6aa0f7ea4b86e42ed6b4a38c1 Mon Sep 17 00:00:00 2001
From: e-271828 <f_s@har.bbiq.jp>
Date: Thu, 16 Apr 2026 22:37:33 +0900
Subject: [PATCH 4/5] fix: replace verbose LLM workaround with simp [hf] per
 reviewer suggestion

---
 Mathlib/Analysis/Calculus/DSlope.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/DSlope.lean b/Mathlib/Analysis/Calculus/DSlope.lean
index d7ebfb7255838a..5a2606e474ecc8 100644
--- a/Mathlib/Analysis/Calculus/DSlope.lean
+++ b/Mathlib/Analysis/Calculus/DSlope.lean
@@ -144,12 +144,7 @@ theorem differentiableAt_dslope_of_ne (h : b ≠ a) :
 
 lemma sub_smul_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (hf : f a = 0) (b : 𝕜) :
     (b - a) • dslope f a b = f b := by
-  by_cases h : b = a
-  · simp [h, hf]
-  · have h_dslope : dslope f a b = (b - a)⁻¹ • f b := by simp [dslope, slope, h, hf]
-    have h_sub_ne_zero : b - a ≠ 0 := sub_ne_zero.mpr h
-    rw [h_dslope, smul_smul]
-    simp [h_sub_ne_zero]
+  simp [hf]
 
 lemma pow_sub_smul_iterate_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (n : ℕ)
     (hf : ∀ k < n, (Function.swap dslope a)^[k] f a = 0) (b : 𝕜) :

From 57b32773838504734dfd60386fc804e25ce09d69 Mon Sep 17 00:00:00 2001
From: e-271828 <f_s@har.bbiq.jp>
Date: Fri, 17 Apr 2026 03:15:38 +0900
Subject: [PATCH 5/5] fix: golf the second lemma using grind per reviewer
 suggestion

---
 Mathlib/Analysis/Calculus/DSlope.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/DSlope.lean b/Mathlib/Analysis/Calculus/DSlope.lean
index 5a2606e474ecc8..b63f46c76b1f1d 100644
--- a/Mathlib/Analysis/Calculus/DSlope.lean
+++ b/Mathlib/Analysis/Calculus/DSlope.lean
@@ -152,8 +152,5 @@ lemma pow_sub_smul_iterate_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (n : ℕ)
   induction n generalizing f with
   | zero => simp
   | succ n ih =>
-    rw [Function.iterate_succ_apply', pow_succ, mul_smul]
-    have hf_n : (Function.swap dslope a)^[n] f a = 0 := hf n (Nat.lt_succ_self n)
-    have hf_lt : ∀ k < n, (Function.swap dslope a)^[k] f a = 0 :=
-      fun k hk => hf k (Nat.lt_trans hk (Nat.lt_succ_self n))
-    rw [sub_smul_dslope_of_zero hf_n b, ih hf_lt]
+    rw [Function.iterate_succ_apply', pow_succ, mul_smul,
+      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]