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
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 : 𝓝[(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₀)

Tactic:
(hst.trans <| nhdsWithin_mono _ <| subset_insert _ _).trans hv

Premises used: Set.Mem, setOf, LE.le.trans, Set.subset_insert, 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₀
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₀)

Tactic:
exact (hst.trans <| nhdsWithin_mono _ <| subset_insert _ _).trans hv

Premises used: LE.le.trans, Set.subset_insert, 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₀
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₀)
z : E
hz : z ∈ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s
⊢ HasFDerivWithinAt (uncurry f) (f' (z, g z)) (insert x₀ s ×ˢ t) (z, g z)

Tactic:
have := hvf' (z, g z) hz.1
-- 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₀)
z : E
hz : z ∈ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s
this : HasFDerivWithinAt (uncurry f) (f' (z, g z)) (insert x₀ s ×ˢ t) (z, g z)
⊢ HasFDerivWithinAt.{u_1, u_3, u_4} (𝕜 := 𝕜) (f z)
    ((fun (z : E) ↦ ((f' (z, g z)).comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.inr 𝕜 E F) : F →L[𝕜] G)) z) t (g z)

Tactic:
this.comp _ (hasFDerivAt_prodMk_right _ _).hasFDerivWithinAt ?_

Premises used: HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.comp, hasFDerivAt_prodMk_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₀)
z : E
hz : z ∈ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s
this : HasFDerivWithinAt (uncurry f) (f' (z, g z)) (insert x₀ s ×ˢ t) (z, g z)
refine_2 : MapsTo (Prod.mk z) t (insert x₀ s ×ˢ t)
⊢ HasFDerivWithinAt.{u_1, u_3, u_4} (𝕜 := 𝕜) (f z)
    ((fun (z : E) ↦ ((f' (z, g z)).comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.inr 𝕜 E F) : F →L[𝕜] G)) z) t (g z)

Tactic:
refine this.comp _ (hasFDerivAt_prodMk_right _ _).hasFDerivWithinAt ?_

Premises used: HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.comp, hasFDerivAt_prodMk_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₀)
z : E
hz : z ∈ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s
this : HasFDerivWithinAt (uncurry f) (f' (z, g z)) (insert x₀ s ×ˢ t) (z, g z)
⊢ MapsTo (Prod.mk z) t (insert x₀ s ×ˢ t)

Tactic:
mapsTo_iff_image_subset.mpr (image_prodMk_subset_prod_right hz.2)

Premises used: Iff.mpr, Set.mapsTo_iff_image_subset, And.right, Set.image_prodMk_subset_prod_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₀)
z : E
hz : z ∈ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s
this : HasFDerivWithinAt (uncurry f) (f' (z, g z)) (insert x₀ s ×ˢ t) (z, g z)
⊢ MapsTo (Prod.mk z) t (insert x₀ s ×ˢ t)

Tactic:
exact mapsTo_iff_image_subset.mpr (image_prodMk_subset_prod_right hz.2)

Premises used: Iff.mpr, Set.mapsTo_iff_image_subset, And.right, Set.image_prodMk_subset_prod_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₀)
⊢ 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₀

Tactic:
(hf'.continuousLinearMap_comp <| (ContinuousLinearMap.compL 𝕜 F (E × F) G).flip
      (ContinuousLinearMap.inr 𝕜 E F)).comp_of_mem_nhdsWithin_image x₀
      (contDiffWithinAt_id.prodMk hg) hst

Premises used: ContinuousLinearMap.comp, ContDiffWithinAt.comp_of_mem_nhdsWithin_image, contDiffWithinAt_id, ContDiffWithinAt.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₀)
⊢ 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₀

Tactic:
exact (hf'.continuousLinearMap_comp <| (ContinuousLinearMap.compL 𝕜 F (E × F) G).flip
      (ContinuousLinearMap.inr 𝕜 E F)).comp_of_mem_nhdsWithin_image x₀
      (contDiffWithinAt_id.prodMk hg) hst

Premises used: ContDiffWithinAt.comp_of_mem_nhdsWithin_image, contDiffWithinAt_id, ContDiffWithinAt.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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
grw : m + 1 ≤ n
grw₁ grw₂ : n ≤ n
⊢ HAdd.hAdd (α := ℕ∞ω) (↑k : ℕ∞ω) 1 ≤ n

Tactic:
grw [hkm, hmn]
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
⊢ Ne (α := ℕ∞ω) (↑k : ℕ∞ω) ∞

Tactic:
simp
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
obtain :
  ∀ (v : Set E) (hv : v ∈ 𝓝[insert x₀ s] x₀) (f' : E → F →L[𝕜] G)
    (hvf' : ∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x))
    (hf' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ f' x) s x₀),
    ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
obtain ⟨v, hv, -, f', hvf', hf'⟩ :=
      (hf.of_le <| by grw [hkm, hmn]).hasFDerivWithinAt_nhds (by simp) (hg.of_le hkm) hgt

Premises used: ContDiffWithinAt.of_le, ContDiffWithinAt.hasFDerivWithinAt_nhds
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
v : Set E
hv : v ∈ 𝓝[insert x₀ s] x₀
f' : E → F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)
hf' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ f' x) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
hf'.congr_of_eventuallyEq_insert ?_

Premises used: ContDiffWithinAt.congr_of_eventuallyEq_insert
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
v : Set E
hv : v ∈ 𝓝[insert x₀ s] x₀
f' : E → F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)
hf' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ f' x) s x₀
refine :
  (𝓝[insert x₀ s] x₀).EventuallyEq (β := F →L[𝕜] G) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) fun (x : E) ↦ f' x
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
refine hf'.congr_of_eventuallyEq_insert ?_

Premises used: ContDiffWithinAt.congr_of_eventuallyEq_insert
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
v : Set E
hv : v ∈ 𝓝[insert x₀ s] x₀
f' : E → F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)
hf' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ f' x) s x₀
h : ∀ a ∈ v, UniqueDiffWithinAt 𝕜 t (g a) → fderivWithin 𝕜 (f a) t (g a) = f' a
⊢ (𝓝[insert x₀ s] x₀).EventuallyEq (β := F →L[𝕜] G) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) fun (x : E) ↦ f' x

Tactic:
filter_upwards [hv, ht]
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
v : Set E
hv : v ∈ 𝓝[insert x₀ s] x₀
f' : E → F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)
hf' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ f' x) s x₀
⊢ ∀ a ∈ v, UniqueDiffWithinAt 𝕜 t (g a) → fderivWithin 𝕜 (f a) t (g a) = f' a

Tactic:
fun y hy h2y => (hvf' y hy).fderivWithin h2y

Premises used: HasFDerivWithinAt.fderivWithin
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
k : ℕ
hkm : (↑k : ℕ∞ω) ≤ m
v : Set E
hv : v ∈ 𝓝[insert x₀ s] x₀
f' : E → F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)
hf' : ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ f' x) s x₀
⊢ ∀ a ∈ v, UniqueDiffWithinAt 𝕜 t (g a) → fderivWithin 𝕜 (f a) t (g a) = f' a

Tactic:
exact fun y hy h2y => (hvf' y hy).fderivWithin h2y

Premises used: HasFDerivWithinAt.fderivWithin
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hgt : t ∈ 𝓝[g '' s] g x₀
⊢ ∀ (k : ℕ),
    (↑k : ℕ∞ω) ≤ m → ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
have : ∀ k : ℕ, k ≤ m → ContDiffWithinAt 𝕜 k (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀ := by
    intro k hkm
    obtain ⟨v, hv, -, f', hvf', hf'⟩ :=
      (hf.of_le <| by grw [hkm, hmn]).hasFDerivWithinAt_nhds (by simp) (hg.of_le hkm) hgt
    refine hf'.congr_of_eventuallyEq_insert ?_
    filter_upwards [hv, ht]
    exact fun y hy h2y => (hvf' y hy).fderivWithin h2y
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ω g s x₀
hmn : HAdd.hAdd (α := ℕ∞ω) ω 1 ≤ n
this :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ n = ω

Tactic:
simpa using hmn
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ω g s x₀
hmn : HAdd.hAdd (α := ℕ∞ω) ω 1 ≤ n
this :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 ω (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)

Tactic:
obtain rfl : n = ω := by simpa using hmn

Premises used: rfl
-- 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ω g s x₀
hmn : HAdd.hAdd (α := ℕ∞ω) ω 1 ≤ n
this :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
hf₁ : ContDiffWithinAt 𝕜 ω (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
⊢ HAdd.hAdd (α := ℕ∞ω) ω 1 ≤ ω

Tactic:
obtain rfl : n = ω := by simpa using hmn

Premises used: rfl
-- 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
x₀ : E
m : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ω g s x₀
this :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
hf : ContDiffWithinAt 𝕜 ω (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hmn : HAdd.hAdd (α := ℕ∞ω) ω 1 ≤ ω
⊢ Ne (α := ℕ∞ω) ω ∞

Tactic:
simp