awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
zero_eq :
  ∀ x ∈ s,
    ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
        (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
      (f x, g x)
fderivWithin :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
          (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m))
          (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := F × G)
            (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin m.succ) ↦ E) (p x m.succ) (q x m.succ)))
          s x
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := F × G) n (fun (y : E) ↦ (f y, g y))
    (fun (y : E) (k : ℕ) ↦ (p y k).prod (M₁ := fun (i : Fin k) ↦ E) (q y k)) s
have cont : ∀ (m : ℕ),
  (↑m : ℕ∞ω) ≤ n →
    ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
      (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m)) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
x : E
hx : x ∈ s
⊢ ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
    (f x, g x)
have zero_eq : ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
    (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
  (ContinuousMultilinearMap.curry0 (p x 0), ContinuousMultilinearMap.curry0 (q x 0))
Tactic: rw [← hf.zero_eq x hx, ← hg.zero_eq x hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 ω f s x
hg : ContDiffWithinAt 𝕜 ω g s x
⊢ ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x
have obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p u)
  (h'p :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
        u),
  ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x
Tactic: obtain ⟨u, hu, p, hp, h'p⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
hg : ContDiffWithinAt 𝕜 ω g s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x
have obtain : ∀ (v : Set E) (hv : v ∈ 𝓝[insert x s] x) (q : E → FormalMultilinearSeries 𝕜 E G) (hq : HasFTaylorSeriesUpToOn ω g q v)
  (h'q :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i)
        v),
  ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x
Tactic: obtain ⟨v, hv, q, hq, h'q⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i) v
⊢ ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x
have refine : ∀ (i : ℕ),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (fun (x : E) ↦ (p x i).prod (M₁ := fun (i : Fin i) ↦ E) (q x i)) (u ∩ v)
Tactic: refine ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right), fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i) v
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (fun (x : E) ↦ (p x i).prod (M₁ := fun (i : Fin i) ↦ E) (q x i)) (u ∩ v)
have change : AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
  (fun (x : E) ↦
    (ContinuousMultilinearMap.prodL 𝕜 (fun (i : Fin i) ↦ E) F G :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F × ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
      (p x i, q x i))
  (u ∩ v)
Tactic: change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.prodL _ _ _ _ (p x i, q x i)) (u ∩ v)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i) v
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (fun (x : E) ↦
      (ContinuousMultilinearMap.prodL 𝕜 (fun (i : Fin i) ↦ E) F G :
          (a :
              ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F × ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
        (p x i, q x i))
    (u ∩ v)
have apply : AnalyticOn 𝕜 (F :=
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F ×
    ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
  (fun (x : E) ↦ (p x i, q x i)) (u ∩ v)
Tactic: apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn _ (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n_1 : ℕ∞ω
s : Set E
f : E → F
g : E → G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) g s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E (F × G)), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (fun (x : E) ↦ (f x, g x)) p u
have rcases : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
  (hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E (F × G)), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (fun (x : E) ↦ (f x, g x)) p u
Tactic: rcases hf m hm with ⟨u, hu, p, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n_1 : ℕ∞ω
s : Set E
f : E → F
g : E → G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) g s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E (F × G)), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (fun (x : E) ↦ (f x, g x)) p u
have rcases : ∀ (v : Set E) (hv : v ∈ 𝓝[insert x s] x) (q : E → FormalMultilinearSeries 𝕜 E G)
  (hq : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) g q v),
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E (F × G)), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (fun (x : E) ↦ (f x, g x)) p u
Tactic: rcases hg m hm with ⟨v, hv, q, hq⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) s x)
    (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
      (iteratedFDerivWithin 𝕜 i g s x))
have h₁ : ∀ (x_1 : (i : Fin i) → E),
  Eq.{u_3 + 1} (α := F)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.fst 𝕜 F G)
            (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) s x) :
          (a : (i : Fin i) → E) → F)
        x_1 :
      F)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.fst 𝕜 F G)
            (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
              (iteratedFDerivWithin 𝕜 i g s x)) :
          (a : (i : Fin i) → E) → F)
        x_1 :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
h₁ :
  ∀ (x_1 : (i : Fin i) → E),
    Eq.{u_3 + 1} (α := F)
      ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.fst 𝕜 F G)
              (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) s x) :
            (a : (i : Fin i) → E) → F)
          x_1 :
        F)
      ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.fst 𝕜 F G)
              (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
                (iteratedFDerivWithin 𝕜 i g s x)) :
            (a : (i : Fin i) → E) → F)
          x_1 :
        F)
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) s x)
    (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
      (iteratedFDerivWithin 𝕜 i g s x))
have h₂ : ∀ (x_1 : (i : Fin i) → E),
  Eq.{u_4 + 1} (α := G)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.snd 𝕜 F G)
            (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) s x) :
          (a : (i : Fin i) → E) → G)
        x_1 :
      G)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.snd 𝕜 F G)
            (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
              (iteratedFDerivWithin 𝕜 i g s x)) :
          (a : (i : Fin i) → E) → G)
        x_1 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
x_1 : (i : Fin i) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.fst 𝕜 F G)
            (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) s x) :
          (a : (i : Fin i) → E) → F)
        x_1 :
      F)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.fst 𝕜 F G)
            (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
              (iteratedFDerivWithin 𝕜 i g s x)) :
          (a : (i : Fin i) → E) → F)
        x_1 :
      F)
have h₁ : Eq.{u_3 + 1} (α := F)
  ((iteratedFDerivWithin 𝕜 i
          (comp (β := F × G) (⇑(ContinuousLinearMap.fst 𝕜 F G : F × G →L[𝕜] F) : (a : F × G) → F) fun (x : E) ↦
            (f x, g x))
          s x :
        (a : (i : Fin i) → E) → F)
      x_1 :
    F)
  ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.fst 𝕜 F G)
          (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
            (iteratedFDerivWithin 𝕜 i g s x)) :
        (a : (i : Fin i) → E) → F)
      x_1 :
    F)
Tactic: rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
x_1 : (i : Fin i) → E
⊢ Eq.{u_4 + 1} (α := G)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.snd 𝕜 F G)
            (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) s x) :
          (a : (i : Fin i) → E) → G)
        x_1 :
      G)
    ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.snd 𝕜 F G)
            (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
              (iteratedFDerivWithin 𝕜 i g s x)) :
          (a : (i : Fin i) → E) → G)
        x_1 :
      G)
have h₂ : Eq.{u_4 + 1} (α := G)
  ((iteratedFDerivWithin 𝕜 i
          (comp (β := F × G) (⇑(ContinuousLinearMap.snd 𝕜 F G : F × G →L[𝕜] G) : (a : F × G) → G) fun (x : E) ↦
            (f x, g x))
          s x :
        (a : (i : Fin i) → E) → G)
      x_1 :
    G)
  ((ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (ContinuousLinearMap.snd 𝕜 F G)
          (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)
            (iteratedFDerivWithin 𝕜 i g s x)) :
        (a : (i : Fin i) → E) → G)
      x_1 :
    G)
Tactic: rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G)) (iteratedFDeriv 𝕜 i (fun (x : E) ↦ (f x, g x)) x)
    (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv 𝕜 i f x) (iteratedFDeriv 𝕜 i g x))
have simp : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
  (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ (f x, g x)) univ x)
  (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f univ x)
    (iteratedFDerivWithin 𝕜 i g univ x))
Tactic: simp only [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hf' : ContDiffOn 𝕜 n f t
hst : s ∪ t = univ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiff 𝕜 n f
have rw : ContDiffOn 𝕜 n f (s ∪ t)
Tactic: rw [← contDiffOn_univ, ← hst]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
⊢ ContDiff 𝕜 n f
have rw : ContDiffOn 𝕜 n f (⋃ (i : ι), s i)
Tactic: rw [← contDiffOn_univ, ← hs']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑0 : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑0 : ℕ∞ω) g s
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ Du) Gu)
      (iteratedFDerivWithin 𝕜 0
        (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
        (↑(Nat.choose 0 i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (0 - i)) ↦ Du) Fu) (iteratedFDerivWithin 𝕜 (0 - i) g s x)
have zero : norm (E := Gu) ((((B : (a : Eu) → Fu →L[𝕜] Gu) (f x) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g x) : Gu) ≤ ‖B‖ * ‖f x‖ * ‖g x‖
Tactic: simp only [norm_iteratedFDerivWithin_zero, zero_add, Finset.range_one,
      Finset.sum_singleton, Nat.choose_self, Nat.cast_one, one_mul, Nat.sub_zero, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ Du) Gu)
      (iteratedFDerivWithin 𝕜 (n + 1)
        (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1 + 1),
        (↑((n + 1).choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
            (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x)
have In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
Tactic: have In : (n : ℕ∞ω) + 1 ≤ n.succ := by simp only [Nat.cast_succ, le_refl]