awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : F
m : Fin i → E
zero :
  ∀ (hi : (↑0 : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin 0 → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin 0) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 0 c s x : (a : (i : Fin 0) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
succ :
  ∀ (i : ℕ)
    (ih :
      ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
        Eq.{u_4 + 1} (α := G)
          ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
          ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G))
    (hi : (↑(i + 1) : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin (i + 1) → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 (i + 1) (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin (i + 1)) → E) → G) m :
        G)
      ((((iteratedFDerivWithin 𝕜 (i + 1) c s x : (a : (i : Fin (i + 1)) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G)
          u :
        G)
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)

Tactic:
induction i generalizing x with
  | zero => simp
  | succ i ih =>
    replace hi : (i : ℕ∞ω) < n := lt_of_lt_of_le (by norm_cast; simp) hi
    have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
      (hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
    have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
      hc.differentiableOn_iteratedFDerivWithin hi hs
    simp only [iteratedFDerivWithin_succ_apply_left]
    rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]
    rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
    rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
      (differentiableWithinAt_const u)]
    rw [fderivWithin_const_apply]
    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]
    rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]

Premises used: ContinuousLinearMap.flip_apply, iteratedFDerivWithin_succ_apply_left, zero_add, ContinuousLinearMap.comp_zero, fderivWithin_const_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : ℕ∞ω
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
x : E
u : F
m : Fin i → E
simp :
  Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) univ x : (a : (i : Fin i) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 i c univ x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
⊢ Eq.{u_4 + 1} (α := G) ((iteratedFDeriv 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) x : (a : (i : Fin i) → E) → G) m : G)
    ((((iteratedFDeriv 𝕜 i c x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)

Tactic:
simp only [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : ℕ∞ω
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
x : E
u : F
m : Fin i → E
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) univ x : (a : (i : Fin i) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 i c univ x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)

Tactic:
iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _)

Premises used: ContDiff.contDiffOn, uniqueDiffOn_univ, Set.mem_univ, iteratedFDerivWithin_clm_apply_const_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : ℕ∞ω
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
x : E
u : F
m : Fin i → E
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) univ x : (a : (i : Fin i) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 i c univ x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)

Tactic:
exact iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _)

Premises used: ContDiff.contDiffOn, uniqueDiffOn_univ, Set.mem_univ, iteratedFDerivWithin_clm_apply_const_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
⊢ insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)

Tactic:
nhdsWithin_mono _ ?_ (nhdsWithin_prod self_mem_nhdsWithin hgt)

Premises used: Set.Mem, setOf, nhdsWithin_prod, self_mem_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
refine : (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
⊢ insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)

Tactic:
refine nhdsWithin_mono _ ?_ (nhdsWithin_prod self_mem_nhdsWithin hgt)

Premises used: nhdsWithin_prod, self_mem_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
simp_rw : s ⊆ (fun (x : E) ↦ (x, g x)) ⁻¹' insert x₀ s ×ˢ (g '' s)
simp_rw₁ : s ⊆ (fun (x : E) ↦ x) ⁻¹' insert x₀ s ∩ g ⁻¹' g '' s
simp_rw₂ : s ⊆ insert x₀ s ∩ g ⁻¹' g '' s
simp_rw₃ : s ⊆ insert x₀ s ∧ s ⊆ g ⁻¹' g '' s
simp_rw₄ : True ∧ s ⊆ g ⁻¹' g '' s
simp_rw₅ : s ⊆ g ⁻¹' g '' s
⊢ (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)

Tactic:
simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]

Premises used: Set.subset_inter_iff, Set.preimage_id', Set.image_subset_iff, Set.subset_insert, Set.subset_preimage_image, true_and, Set.mk_preimage_prod
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
⊢ insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)

Tactic:
have hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀) := by
    refine nhdsWithin_mono _ ?_ (nhdsWithin_prod self_mem_nhdsWithin hgt)
    simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
obtain :
  ∀ (v : Set (E × F)) (hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀))
    (hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)) (f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v)
    (f' : E × F → E × F →L[𝕜] G) (hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x)
    (hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)),
    ∃ v ∈ 𝓝[insert x₀ s] x₀,
      v ⊆ insert x₀ s ∧
        ∃ (f' : E → F →L[𝕜] G),
          (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧
            ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) n (fun (x : E) ↦ f' x) s x₀
⊢ ∃ v ∈ 𝓝[insert x₀ s] x₀,
    v ⊆ insert x₀ s ∧
      ∃ (f' : E → F →L[𝕜] G),
        (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧
          ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) n (fun (x : E) ↦ f' x) s x₀

Tactic:
obtain ⟨v, hv, hvs, f_an, f', hvf', hf'⟩ :=
    (contDiffWithinAt_succ_iff_hasFDerivWithinAt' hn).mp hf

Premises used: contDiffWithinAt_succ_iff_hasFDerivWithinAt', Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
⊢ ∃ v ∈ 𝓝[insert x₀ s] x₀,
    v ⊆ insert x₀ s ∧
      ∃ (f' : E → F →L[𝕜] G),
        (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧
          ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) n (fun (x : E) ↦ f' x) s x₀

Tactic:
⟨(fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s, ?_, inter_subset_right, fun z =>
      (f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F), ?_, ?_⟩

Premises used: ContinuousLinearMap.comp, Insert.insert, Prod.mk, Inter.inter, ContinuousLinearMap.inr, Set.preimage, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
refine_1 : (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s ∈ 𝓝[insert x₀ s] x₀
refine_2 :
  ∀ x ∈ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s,
    HasFDerivWithinAt.{u_1, u_3, u_4} (𝕜 := 𝕜) (f x)
      ((fun (z : E) ↦ ((f' (z, g z)).comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.inr 𝕜 E F) : F →L[𝕜] G)) x) t (g x)
refine_3 :
  ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) n
    (fun (x : E) ↦
      (fun (z : E) ↦ ((f' (z, g z)).comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.inr 𝕜 E F) : F →L[𝕜] G)) x)
    s x₀
⊢ ∃ v ∈ 𝓝[insert x₀ s] x₀,
    v ⊆ insert x₀ s ∧
      ∃ (f' : E → F →L[𝕜] G),
        (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧
          ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) n (fun (x : E) ↦ f' x) s x₀

Tactic:
refine
    ⟨(fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s, ?_, inter_subset_right, fun z =>
      (f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F), ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s ∈ 𝓝[insert x₀ s] x₀

Tactic:
inter_mem ?_ self_mem_nhdsWithin

Premises used: Filter.inter_mem, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
refine_1 : (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[insert x₀ s] x₀
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s ∈ 𝓝[insert x₀ s] x₀

Tactic:
refine inter_mem ?_ self_mem_nhdsWithin

Premises used: Filter.inter_mem, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
⊢ (x₀, g x₀) ∈ v

Tactic:
have := mem_of_mem_nhdsWithin (mem_insert _ _) hv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[insert x₀ s] x₀

Tactic:
mem_nhdsWithin_insert.mpr ⟨this, ?_⟩

Premises used: Iff.mpr, mem_nhdsWithin_insert, And.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
refine_1 : (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[s] x₀
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[insert x₀ s] x₀

Tactic:
refine mem_nhdsWithin_insert.mpr ⟨this, ?_⟩

Premises used: Iff.mpr, mem_nhdsWithin_insert, And.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[s] x₀

Tactic:
(continuousWithinAt_id.prodMk hg.continuousWithinAt).preimage_mem_nhdsWithin' ?_

Premises used: Set.Mem, setOf, continuousWithinAt_id, ContinuousWithinAt.preimage_mem_nhdsWithin', ContDiffWithinAt.continuousWithinAt, ContinuousWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
refine_1 : v ∈ 𝓝[(fun (x : E) ↦ (id x, g x)) '' s] (id x₀, g x₀)
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[s] x₀

Tactic:
refine (continuousWithinAt_id.prodMk hg.continuousWithinAt).preimage_mem_nhdsWithin' ?_

Premises used: continuousWithinAt_id, ContinuousWithinAt.preimage_mem_nhdsWithin', ContDiffWithinAt.continuousWithinAt, ContinuousWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
refine_1 :
  ∀ (hst : 𝓝[(fun (x : E) ↦ (x, g x)) '' s] (x₀, g x₀) ≤ 𝓝[insert x₀ s ×ˢ t] (x₀, g x₀)) (v : Set (E × F))
    (hv : 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀) ≤ 𝓝[v] (x₀, g x₀))
    (hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)) (f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v)
    (f' : E × F → E × F →L[𝕜] G) (hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x)
    (hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)) (this : (x₀, g x₀) ∈ v),
    𝓝[(fun (x : E) ↦ (id x, g x)) '' s] (id x₀, g x₀) ≤ 𝓝[v] (id x₀, g x₀)
⊢ v ∈ 𝓝[(fun (x : E) ↦ (id x, g x)) '' s] (id x₀, g x₀)

Tactic:
rw [← nhdsWithin_le_iff] at hst hv ⊢

Premises used: nhdsWithin_le_iff