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
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 ≤ ω
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) ω (fun (x : E) ↦ f' x) s x₀),
    ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) ω (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) ω (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
obtain ⟨v, hv, -, f', hvf', hf'⟩ := hf.hasFDerivWithinAt_nhds (by simp) hg hgt

Premises used: 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 : ℕ∞ω
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 ≤ ω
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) ω (fun (x : E) ↦ f' x) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) ω (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 : ℕ∞ω
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 ≤ ω
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) ω (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) ω (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 : ℕ∞ω
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 ≤ ω
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) ω (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 : ℕ∞ω
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 ≤ ω
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) ω (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 : ℕ∞ω
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 ≤ ω
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) ω (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₀)
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₀
rw : ∀ (n : ℕ), ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑n : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) ∞ (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
rw [contDiffWithinAt_infty]

Premises used: contDiffWithinAt_infty
-- 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₀
k : ℕ
⊢ LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ∞

Tactic:
exact_mod_cast le_top

Premises used: le_top
-- 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 : ℕ), ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑n : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
exact fun k ↦ this k (by exact_mod_cast le_top)
-- 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_1 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₀
m : ℕ
hg : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) g s x₀
hmn : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≤ n
this :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω) →
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑m : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
this _ le_rfl

Premises used: le_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_1 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₀
m : ℕ
hg : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) g s x₀
hmn : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≤ n
this :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω) →
      ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑m : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
exact this _ le_rfl

Premises used: le_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₀)
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₀
this :
  ∀ (k : ℕ),
    (↑k : ℕ∞ω) ≤ m → ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
match m with
  | ω =>
    obtain rfl : n = ω := by simpa using hmn
    obtain ⟨v, hv, -, f', hvf', hf'⟩ := hf.hasFDerivWithinAt_nhds (by simp) hg hgt
    refine hf'.congr_of_eventuallyEq_insert ?_
    filter_upwards [hv, ht]
    exact fun y hy h2y => (hvf' y hy).fderivWithin h2y
  | ∞ =>
    rw [contDiffWithinAt_infty]
    exact fun k ↦ this k (by exact_mod_cast le_top)
  | (m : ℕ) => exact this _ le_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₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hmn : m + 1 ≤ n
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
hf.fderivWithin'' hg ht hmn <| mem_of_superset self_mem_nhdsWithin <| image_subset_iff.mpr hst

Premises used: Iff.mpr, ContDiffWithinAt.fderivWithin'', self_mem_nhdsWithin, Set.image_subset_iff, Filter.mem_of_superset
-- 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) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)

Tactic:
rw [← insert_eq_self.mpr hx₀] at hf

Premises used: Iff.mpr, Set.insert_eq_self
-- 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) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
hf₁ : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
⊢ ContDiffWithinAt 𝕜 m g s x₀

Tactic:
rw [← insert_eq_self.mpr hx₀] at hf

Premises used: Iff.mpr, Set.insert_eq_self
-- 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) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
hf₁ : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg₁ : ContDiffWithinAt 𝕜 m g s x₀
⊢ UniqueDiffOn 𝕜 t

Tactic:
rw [← insert_eq_self.mpr hx₀] at hf

Premises used: Iff.mpr, Set.insert_eq_self
-- 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) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
hf₁ : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg₁ : ContDiffWithinAt 𝕜 m g s x₀
ht₁ : UniqueDiffOn 𝕜 t
⊢ m + 1 ≤ n

Tactic:
rw [← insert_eq_self.mpr hx₀] at hf

Premises used: Iff.mpr, Set.insert_eq_self
-- 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) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
hf₁ : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg₁ : ContDiffWithinAt 𝕜 m g s x₀
ht₁ : UniqueDiffOn 𝕜 t
hmn₁ : m + 1 ≤ n
⊢ x₀ ∈ s

Tactic:
rw [← insert_eq_self.mpr hx₀] at hf

Premises used: Iff.mpr, Set.insert_eq_self
-- 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) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
hf₁ : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg₁ : ContDiffWithinAt 𝕜 m g s x₀
ht₁ : UniqueDiffOn 𝕜 t
hmn₁ : m + 1 ≤ n
hx₁ : x₀ ∈ s
⊢ s ⊆ g ⁻¹' t

Tactic:
rw [← insert_eq_self.mpr hx₀] at hf

Premises used: Iff.mpr, Set.insert_eq_self
-- 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 : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
hf.fderivWithin' hg ?_ hmn hst

Premises used: ContDiffWithinAt.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 : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
refine : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
refine hf.fderivWithin' hg ?_ hmn hst

Premises used: ContDiffWithinAt.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 : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
rw : ∀ᶠ (x : E) in 𝓝[s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
⊢ ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)

Tactic:
rw [insert_eq_self.mpr hx₀]

Premises used: Iff.mpr, Set.insert_eq_self
-- 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 : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, UniqueDiffWithinAt 𝕜 t (g x)

Tactic:
eventually_of_mem self_mem_nhdsWithin fun x hx => ht _ (hst hx)

Premises used: Filter.eventually_of_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
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 : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, UniqueDiffWithinAt 𝕜 t (g x)

Tactic:
exact eventually_of_mem self_mem_nhdsWithin fun x hx => ht _ (hst hx)

Premises used: Filter.eventually_of_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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g k : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
hk : ContDiffWithinAt 𝕜 m k s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) m (fun (x : E) ↦ (fderivWithin 𝕜 (f x) t (g x) : (a : F) → G) (k x)) s x₀

Tactic:
(contDiff_fst.clm_apply contDiff_snd).contDiffAt.comp_contDiffWithinAt x₀
    ((hf.fderivWithin hg ht hmn hx₀ hst).prodMk hk)

Premises used: contDiff_fst, ContDiffAt.comp_contDiffWithinAt, ContDiff.clm_apply, ContDiffWithinAt.fderivWithin, contDiff_snd, ContDiffWithinAt.prodMk, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : Set E
f : E → F
x₀ : E
m n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx₀s : x₀ ∈ s
rw rw₁ : s ⊆ s
⊢ s ⊆ (fun (x : E) ↦ x) ⁻¹' s

Tactic:
rw [preimage_id']

Premises used: Set.preimage_id'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
m n : ℕ∞ω
f : F → G
k : F → F
s : Set F
x₀ : F
hf : ContDiffWithinAt 𝕜 n f s x₀
hk : ContDiffWithinAt 𝕜 m k s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx₀s : x₀ ∈ s
rw rw₁ : s ⊆ s
⊢ s ⊆ (fun (x : F) ↦ x) ⁻¹' s

Tactic:
rw [preimage_id']

Premises used: Set.preimage_id'