awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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.{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:
((h'p i).mono inter_subset_left).prod ((h'q i).mono inter_subset_right)

Premises used: Set.inter_subset_left, AnalyticOn.prod, Set.inter_subset_right, AnalyticOn.mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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.{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:
exact ((h'p i).mono inter_subset_left).prod ((h'q i).mono inter_subset_right)

Premises used: Set.inter_subset_left, AnalyticOn.prod, Set.inter_subset_right, AnalyticOn.mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
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
⊢ ∃ 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⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
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
⊢ ∃ 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⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
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:
⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right)⟩

Premises used: Filter.inter_mem, HasFTaylorSeriesUpToOn.mono, Set.inter_subset_left, Inter.inter, HasFTaylorSeriesUpToOn.prodMk, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
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:
exact ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right)⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt 𝕜 (F := F × G) n (fun (x : E) ↦ (f x, g x)) s x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, hp, h'p⟩ := hf
    obtain ⟨v, hv, q, hq, h'q⟩ := hg
    refine ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right), fun i ↦ ?_⟩
    change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.prodL _ _ _ _ (p x i, q x i)) (u ∩ v)
    apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn _ (Set.mapsTo_univ _ _)
    exact ((h'p i).mono inter_subset_left).prod ((h'q i).mono inter_subset_right)
  | (n : ℕ∞) =>
    intro m hm
    rcases hf m hm with ⟨u, hu, p, hp⟩
    rcases hg m hm with ⟨v, hv, q, hq⟩
    exact ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right)⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn 𝕜 (F := F × G) n (fun (x : E) ↦ (f x, g x)) s

Tactic:
fun x hx =>
  (hf x hx).prodMk (hg x hx)

Premises used: ContDiffOn, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
⊢ ContDiffAt 𝕜 (F := F × G) n (fun (x : E) ↦ (f x, g x)) x

Tactic:
contDiffWithinAt_univ.1 <| hf.contDiffWithinAt.prodMk hg.contDiffWithinAt

Premises used: contDiffWithinAt_univ, Iff.mp, ContDiffWithinAt.prodMk, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 (F := F × G) n fun (x : E) ↦ (f x, g x)

Tactic:
contDiffOn_univ.1 <| hf.contDiffOn.prodMk hg.contDiffOn

Premises used: ContDiff.contDiffOn, Iff.mp, ContDiffOn.prodMk, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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)
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
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)
⊢ 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:
rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]

Premises used: ContinuousLinearMap.iteratedFDerivWithin_comp_left, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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)
    ((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:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
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)
⊢ 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:
rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]

Premises used: ContinuousLinearMap.iteratedFDerivWithin_comp_left, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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)
    ((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:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
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))
⊢ 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))

Tactic:
simp only [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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))
    (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:
iteratedFDerivWithin_prodMk hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
    (Set.mem_univ _) hi

Premises used: iteratedFDerivWithin_prodMk, uniqueDiffOn_univ, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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))
    (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:
exact iteratedFDerivWithin_prodMk hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
    (Set.mem_univ _) hi

Premises used: iteratedFDerivWithin_prodMk, uniqueDiffOn_univ, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f (s ∪ t) x

Tactic:
(hf x hx).contDiffAt (hs.mem_nhds hx) |>.contDiffWithinAt

Premises used: ContDiffWithinAt.contDiffAt, IsOpen.mem_nhds, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f (s ∪ t) x

Tactic:
exact (hf x hx).contDiffAt (hs.mem_nhds hx) |>.contDiffWithinAt

Premises used: ContDiffWithinAt.contDiffAt, IsOpen.mem_nhds, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
x : E
hx : x ∈ t
⊢ ContDiffWithinAt 𝕜 n f (s ∪ t) x

Tactic:
(hf' x hx).contDiffAt (ht.mem_nhds hx) |>.contDiffWithinAt

Premises used: ContDiffWithinAt.contDiffAt, IsOpen.mem_nhds, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
x : E
hx : x ∈ t
⊢ ContDiffWithinAt 𝕜 n f (s ∪ t) x

Tactic:
exact (hf' x hx).contDiffAt (ht.mem_nhds hx) |>.contDiffWithinAt

Premises used: ContDiffWithinAt.contDiffAt, IsOpen.mem_nhds, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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 : ℕ∞ω
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiffOn 𝕜 n f (s ∪ t) ↔ ContDiffOn 𝕜 n f s ∧ ContDiffOn 𝕜 n f t

Tactic:
⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right⟩,
   fun ⟨hfs, hft⟩ ↦ ContDiffOn.union_of_isOpen hfs hft hs ht⟩

Premises used: _private.0.contDiffOn_union_iff_of_isOpen.match_1, Set.subset_union_right, ContDiffOn.mono, ContDiffOn, Set.subset_union_left, And.intro, ContDiffOn.union_of_isOpen, Iff.intro, Union.union