awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
t : Set E
x : E
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
h : ∀ i_1 ∈ insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ insert i s, f i x) t x
have insert : ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x + ∑ i ∈ s, f i x) t x
Tactic: simp only [is, Finset.sum_insert, not_false_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
t : Set E
x : E
h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
have empty : ∀
  (h :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
  ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ ∅, f i x) t x
Tactic: induction s using Finset.induction_on with
  | empty => simp [contDiffWithinAt_const]
  | insert i s is IH =>
    simp only [is, Finset.sum_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
t : Set E
x : E
h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ ∅, f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
have insert : ∀ (i : ι) (s : Finset ι) (is : i ∉ s)
  (IH :
    ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
      ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x)
  (h : ∀ i_1 ∈ insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x),
  ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ insert i s, f i x) t x
Tactic: induction s using Finset.induction_on with
  | empty => simp [contDiffWithinAt_const]
  | insert i s is IH =>
    simp only [is, Finset.sum_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
t : Set E
x : E
h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
have empty : ∀
  (h :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
  ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ ∅, f i x) t x
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp [contDiffWithinAt_const]
  | insert i s is IH =>
    simp only [is, Finset.sum_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
t : Set E
x : E
h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ ∅, f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
have insert : ∀ (i : ι) (s : Finset ι) (is : i ∉ s)
  (IH :
    ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
      ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x)
  (h : ∀ i_1 ∈ insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x),
  ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ insert i s, f i x) t x
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp [contDiffWithinAt_const]
  | insert i s is IH =>
    simp only [is, Finset.sum_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (x : E) ↦ f i x
⊢ ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (x : E) ↦ ∑ i ∈ s, f i x
have simp : ∀ (h : ∀ i ∈ s, ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) univ),
  ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) univ
Tactic: simp only [← contDiffOn_univ] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
  (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
Tactic: rw [(by aesop : (∑ j ∈ u, f j) = (fun x ↦ ∑ j ∈ u, f j x))]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
h : ∀ j ∈ Finset.cons a u ha, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ Finset.cons a u ha, f j x) s x)
    (∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x)
have h₁ : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x
Tactic: simp only [Finset.mem_cons, forall_eq_or_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
h : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ Finset.cons a u ha, f j x) s x)
    (∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x)
have cons : iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ f a x + ∑ j ∈ u, f j x) s x =
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
Tactic: simp only [Finset.sum_cons]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
h : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ f a x + ∑ j ∈ u, f j x) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
have cons : HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (f a) s x) (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ i ∈ u, f i x) s x) =
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
Tactic: rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
h : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x
cons :
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ i ∈ u, f i x) s x) =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
⊢ iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ f a x + ∑ j ∈ u, f j x) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
have cons₁ : HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x) =
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
Tactic: rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
have empty : ∀ (h : ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ ∅, f j x) s x) (∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x)
Tactic: induction u using Finset.cons_induction with
  | empty => simp
  | cons a u ha IH =>
    simp only [Finset.mem_cons, forall_eq_or_imp] at h
    simp only [Finset.sum_cons]
    rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
empty :
  ∀ (h : ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ ∅, f j x) s x) (∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
have cons : ∀ (a : ι) (u : Finset ι) (ha : a ∉ u)
  (IH :
    ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
      Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x))
  (h : ∀ j ∈ Finset.cons a u ha, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ Finset.cons a u ha, f j x) s x)
    (∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x)
Tactic: induction u using Finset.cons_induction with
  | empty => simp
  | cons a u ha IH =>
    simp only [Finset.mem_cons, forall_eq_or_imp] at h
    simp only [Finset.sum_cons]
    rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (z : E) ↦ ∑ j ∈ u, f j z) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
have h₁ : ∀ (x : E), Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x) ((∑ j ∈ u, f j) x)
Tactic: convert! iteratedFDerivWithin_sum_apply hs hx h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
x_1 : E
⊢ Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) ((∑ j ∈ u, f j) x_1)
have h₁ : Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) (∑ c ∈ u, f c x_1)
Tactic: rw [Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n (∑ j ∈ u, f j) x)
    (∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x)
have simp : Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
  (iteratedFDerivWithin 𝕜 n (∑ j ∈ u, f j) univ x) (∑ x_1 ∈ u, iteratedFDerivWithin 𝕜 n (f x_1) univ x)
Tactic: simp only [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n (fun (z : E) ↦ ∑ j ∈ u, f j z) x) (∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x)
have h₁ : ∀ (x : E), Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x) ((∑ j ∈ u, f j) x)
Tactic: convert! iteratedFDeriv_sum_apply h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
x_1 : E
⊢ Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) ((∑ j ∈ u, f j) x_1)
have h₁ : Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) (∑ c ∈ u, f c x_1)
Tactic: rw [Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 n (f • g) x
have hf₁ : ContDiffWithinAt 𝕜 n f univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
hf₁ : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffAt 𝕜 n (f • g) x
have hg₁ : ContDiffWithinAt 𝕜 n g univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ c • f y) x
have hf₁ : ContDiffWithinAt 𝕜 n f univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffAt 𝕜 n f x
v : F
⊢ ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) x
have rw : ∀ (hf : ContDiffWithinAt 𝕜 n f univ x) (v : F),
  ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf, v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑0 : ℕ∞ω) f
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDeriv 𝕜 0 fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
      (iteratedFDeriv 𝕜 0 f (a • x))
have zero : ∀ (x : E) (x_1 : (i : Fin 0) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 0 (fun (z : E) ↦ f (a • z)) x : (a : (i : Fin 0) → E) → F) x_1 : F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
            (iteratedFDeriv 𝕜 0 f (a • x)) :
          (a : (i : Fin 0) → E) → F)
        x_1 :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
i_1 : ℕ
a : 𝕜
i : ℕ
hi :
  ∀ (hf : ContDiff 𝕜 (↑i : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
        (iteratedFDeriv 𝕜 i f (a • x))
hf : ContDiff 𝕜 (↑(i + 1) : ℕ∞ω) f
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (i + 1) fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
      (iteratedFDeriv 𝕜 (i + 1) f (a • x))
have succ : ∀ (v : E) (x : (i : Fin (i + 1)) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (i + 1) (fun (z : E) ↦ f (a • z)) v : (a : (i : Fin (i + 1)) → E) → F) x : F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
            (iteratedFDeriv 𝕜 (i + 1) f (a • v)) :
          (a : (i : Fin (i + 1)) → E) → F)
        x :
      F)
Tactic: ext v