awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
inl : k ≤ i → (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
have inr : i < k → (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
Tactic: cases le_or_gt k i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
h_1 : k ≤ i
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
have inl : i + 1 = k + 1 + (i - k) ∨ i < k
Tactic: simp [Nat.descFactorial, ← add_mul, *]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
have this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
Tactic: have : ((i + 1).descFactorial (k + 1)) =
        (k + 1) * (i.descFactorial k) + (i.descFactorial (k + 1)) := by
      rw [Nat.succ_descFactorial_succ]
      cases le_or_gt k i <;> simp [Nat.descFactorial, ← add_mul, *]; lia
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
have succ : ∀ (hik : i ≤ k),
  ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
Tactic: obtain hik | hik := le_or_gt i k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
succ :
  ∀ (hik : i ≤ k),
    ∑ i_1 ∈ Finset.range (k + 1 + 1),
        HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
          iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
      (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
have succ₁ : ∀ (hik : k < i),
  ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
Tactic: obtain hik | hik := le_or_gt i k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 0
have simp : ∀ x < k, ¬k + 1 - x = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 1
have simp : ∀ x < k, ¬k + 1 - x = 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 0
have simp : ∀ x < k, ¬k + 1 - x = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 1
have simp : ∀ x < k, ¬k + 1 - x = 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
have succ : HAdd.hAdd (α := 𝕜) (↑k : 𝕜) 1 * ((↑(i.descFactorial k) : 𝕜) * x ^ (i - (k + 1) + 1)) +
    (↑(i.descFactorial (k + 1)) : 𝕜) * x ^ (i - (k + 1)) * x =
  (HAdd.hAdd (α := 𝕜) (↑k : 𝕜) 1 * (↑(i.descFactorial k) : 𝕜) + (↑(i.descFactorial (k + 1)) : 𝕜)) *
    x ^ (i - (k + 1) + 1)
Tactic: simp +contextual [IH, iteratedDerivWithin_fun_id, h, hx, Finset.sum_range_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 0 by simp; lia, -Nat.descFactorial_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 1 by simp; lia, this,
        Nat.descFactorial_eq_zero_iff_lt.mpr, hik,
        show k < i → i - k = (i - (k + 1) + 1) by lia]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
m k : ℕ
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ m) s x = (↑(m.descFactorial k) : 𝕜) * x ^ (m - k)
have zero : ∀ (k : ℕ),
  iteratedDerivWithin k (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x = (↑(Nat.descFactorial 0 k) : 𝕜) * x ^ (0 - k)
Tactic: induction m generalizing k with
  | zero => cases k <;> simp [iteratedDerivWithin_const]
  | succ i IH =>
    obtain (_ | k) := k
    · simp
    simp only [pow_succ]
    refine (iteratedDerivWithin_mul hx h (by fun_prop) (by fun_prop)).trans ?_
    have : ((i + 1).descFactorial (k + 1)) =
        (k + 1) * (i.descFactorial k) + (i.descFactorial (k + 1)) := by
      rw [Nat.succ_descFactorial_succ]
      cases le_or_gt k i <;> simp [Nat.descFactorial, ← add_mul, *]; lia
    obtain hik | hik := le_or_gt i k <;>
      simp +contextual [IH, iteratedDerivWithin_fun_id, h, hx, Finset.sum_range_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 0 by simp; lia, -Nat.descFactorial_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 1 by simp; lia, this,
        Nat.descFactorial_eq_zero_iff_lt.mpr, hik,
        show k < i → i - k = (i - (k + 1) + 1) by lia]; ring
Cleared hypotheses: m, k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
m k : ℕ
zero :
  ∀ (k : ℕ),
    iteratedDerivWithin k (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x = (↑(Nat.descFactorial 0 k) : 𝕜) * x ^ (0 - k)
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ m) s x = (↑(m.descFactorial k) : 𝕜) * x ^ (m - k)
have succ : ∀ (i : ℕ) (IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k))
  (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial k) : 𝕜) * x ^ (i + 1 - k)
Tactic: induction m generalizing k with
  | zero => cases k <;> simp [iteratedDerivWithin_const]
  | succ i IH =>
    obtain (_ | k) := k
    · simp
    simp only [pow_succ]
    refine (iteratedDerivWithin_mul hx h (by fun_prop) (by fun_prop)).trans ?_
    have : ((i + 1).descFactorial (k + 1)) =
        (k + 1) * (i.descFactorial k) + (i.descFactorial (k + 1)) := by
      rw [Nat.succ_descFactorial_succ]
      cases le_or_gt k i <;> simp [Nat.descFactorial, ← add_mul, *]; lia
    obtain hik | hik := le_or_gt i k <;>
      simp +contextual [IH, iteratedDerivWithin_fun_id, h, hx, Finset.sum_range_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 0 by simp; lia, -Nat.descFactorial_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 1 by simp; lia, this,
        Nat.descFactorial_eq_zero_iff_lt.mpr, hik,
        show k < i → i - k = (i - (k + 1) + 1) by lia]; ring
Cleared hypotheses: m, k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ContDiff 𝕜 (↑n : WithTop ℕ∞) f
c : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (x : 𝕜) ↦ f (c * x)) fun (x : 𝕜) ↦ c ^ n • iteratedDeriv n f (c * x)
have h₁ : ∀ (x : 𝕜), iteratedDeriv n (fun (x : 𝕜) ↦ f (c * x)) x = c ^ n • iteratedDeriv n f (c * x)
Tactic: funext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
⊢ iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0
have zero : iteratedDeriv 0 id x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
zero : iteratedDeriv 0 id x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0
⊢ iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0
have succ : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) id x =
  if HAdd.hAdd (α := ℕ) 0 1 = 0 then x else if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
zero : iteratedDeriv 0 id x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0
succ :
  iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) id x =
    if HAdd.hAdd (α := ℕ) 0 1 = 0 then x else if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0
⊢ iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0
have succ₁ : ∀ (n : ℕ), iteratedDeriv (n + 1 + 1) id x = if n + 1 + 1 = 0 then x else if n + 1 + 1 = 1 then 1 else 0
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
have inl : ∀ (h : n < m), Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
Tactic: obtain h | h | h := lt_trichotomy n m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ
inl :
  ∀ (h : n < m),
    Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
have inr : ∀ (h : n = m), Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
Tactic: obtain h | h | h := lt_trichotomy n m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ
inl :
  ∀ (h : n < m),
    Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
inr :
  ∀ (h : n = m),
    Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
have inr₁ : ∀ (h : m < n), Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
Tactic: obtain h | h | h := lt_trichotomy n m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
⊢ iteratedDeriv n f x = iteratedDeriv n g x
have simp : Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
  ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: simp only [← iteratedDerivWithin_univ, iteratedDerivWithin_eq_iteratedFDerivWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
⊢ Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
have rw : Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
  ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: rw [(hfg.filter_mono nhdsWithin_le_nhds).iteratedFDerivWithin_eq hfg.eq_of_nhds n]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
⊢ EqOn (iteratedDeriv n f) (iteratedDeriv n g) s
have refine : ∀ (x : 𝕜) (hx : x ∈ s), f =ᶠ[𝓝 x] g
Tactic: refine fun x hx ↦ Filter.EventuallyEq.iteratedDeriv_eq n ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
x : 𝕜
hx : x ∈ s
⊢ f =ᶠ[𝓝 x] g
have h : ∀ (a : 𝕜) (ha : a ∈ s), f a = g a
Tactic: filter_upwards [IsOpen.mem_nhds hs hx] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv n f (s + t)
have zero : Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (s + t)
Tactic: induction n with
  | zero => simp only [iteratedDeriv_zero]
  | succ n IH =>
    simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_const_add _ s
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
zero : Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (s + t)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv n f (s + t)
have succ : ∀ (n : ℕ)
  (IH : Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv n f (s + t)),
  Eq (α := (x : 𝕜) → F) (iteratedDeriv (n + 1) fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv (n + 1) f (s + t)
Tactic: induction n with
  | zero => simp only [iteratedDeriv_zero]
  | succ n IH =>
    simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_const_add _ s
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv n f (t + s)
have zero : Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (t + s)
Tactic: induction n with
  | zero => simp only [iteratedDeriv_zero]
  | succ n IH =>
    simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
zero : Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (t + s)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv n f (t + s)
have succ : ∀ (n : ℕ)
  (IH : Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv n f (t + s)),
  Eq (α := (x : 𝕜) → F) (iteratedDeriv (n + 1) fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv (n + 1) f (t + s)
Tactic: induction n with
  | zero => simp only [iteratedDeriv_zero]
  | succ n IH =>
    simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x)
hf : ∀ i_1 ∈ insert i t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i_1) s x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ insert i t, f i) s x)
    (∑ i ∈ insert i t, iteratedDerivWithin n (f i) s x)
have hf₁ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f x_1) s x
Tactic: rw [forall_mem_insert] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x)
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f x_1) s x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ insert i t, f i) s x)
    (∑ i ∈ insert i t, iteratedDerivWithin n (f i) s x)
have insert : ∀
  (IH :
    ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
      Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x)
        (∑ i ∈ t, iteratedDerivWithin n (f i) s x)),
  iteratedDerivWithin n (f i + fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x =
    iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
Tactic: simp only [sum_insert hi, sum_fn] at IH ⊢
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f x_1) s x
IH :
  ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x)
      (∑ i ∈ t, iteratedDerivWithin n (f i) s x)
⊢ iteratedDerivWithin n (f i + fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x =
    iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
have insert : iteratedDerivWithin n (f i) s x + iteratedDerivWithin n (fun (x : 𝕜) ↦ ∑ i ∈ t, f i x) s x =
  iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
Tactic: rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f x_1) s x
IH :
  ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x)
      (∑ i ∈ t, iteratedDerivWithin n (f i) s x)
insert :
  iteratedDerivWithin n (f i) s x + iteratedDerivWithin n (fun (x : 𝕜) ↦ ∑ i ∈ t, f i x) s x =
    iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
⊢ iteratedDerivWithin n (f i + fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x =
    iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
have insert₁ : iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x =
  iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
Tactic: rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]