awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
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.{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)
have this : HasFDerivWithinAt (uncurry f) (f' (z, g z)) (insert x₀ s ×ˢ t) (z, g z)
Tactic: have := hvf' (z, g z) hz.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
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)
have refine_2 : MapsTo (Prod.mk z) t (insert x₀ s ×ˢ t)
Tactic: refine this.comp _ (hasFDerivAt_prodMk_right _ _).hasFDerivWithinAt ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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
⊢ HAdd.hAdd (α := ℕ∞ω) (↑k : ℕ∞ω) 1 ≤ n
have grw₁ : n ≤ n
Tactic: grw [hkm, hmn]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑k : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
have 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₀
Tactic: obtain ⟨v, hv, -, f', hvf', hf'⟩ :=
      (hf.of_le <| by grw [hkm, hmn]).hasFDerivWithinAt_nhds (by simp) (hg.of_le hkm) hgt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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₀
have refine : (𝓝[insert x₀ s] x₀).EventuallyEq (β := F →L[𝕜] G) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) fun (x : E) ↦ f' x
Tactic: refine hf'.congr_of_eventuallyEq_insert ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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₀
⊢ (𝓝[insert x₀ s] x₀).EventuallyEq (β := F →L[𝕜] G) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) fun (x : E) ↦ f' x
have h : ∀ a ∈ v, UniqueDiffWithinAt 𝕜 t (g a) → fderivWithin 𝕜 (f a) t (g a) = f' a
Tactic: filter_upwards [hv, ht]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
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₀
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
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 𝕜 (F := F →L[𝕜] G) ω (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
have hf₁ : ContDiffWithinAt 𝕜 ω (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
Tactic: obtain rfl : n = ω := by simpa using hmn
Cleared hypotheses: n, hf, hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
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₀)
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) ω (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
have hmn₁ : HAdd.hAdd (α := ℕ∞ω) ω 1 ≤ ω
Tactic: obtain rfl : n = ω := by simpa using hmn
Cleared hypotheses: n, hf, hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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 ≤ ω
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) ω (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
have 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₀
Tactic: obtain ⟨v, hv, -, f', hvf', hf'⟩ := hf.hasFDerivWithinAt_nhds (by simp) hg hgt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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₀
have refine : (𝓝[insert x₀ s] x₀).EventuallyEq (β := F →L[𝕜] G) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) fun (x : E) ↦ f' x
Tactic: refine hf'.congr_of_eventuallyEq_insert ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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₀
⊢ (𝓝[insert x₀ s] x₀).EventuallyEq (β := F →L[𝕜] G) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) fun (x : E) ↦ f' x
have h : ∀ a ∈ v, UniqueDiffWithinAt 𝕜 t (g a) → fderivWithin 𝕜 (f a) t (g a) = f' a
Tactic: filter_upwards [hv, ht]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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 𝕜 (F := F →L[𝕜] G) ∞ (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
have rw : ∀ (n : ℕ), ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) (↑n : ℕ∞ω) (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
Tactic: rw [contDiffWithinAt_infty]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
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 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
have hf₁ : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
Tactic: rw [← insert_eq_self.mpr hx₀] at hf
Cleared hypotheses: hf, hg, ht, hmn, hx₀, hst
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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₀
have refine : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
Tactic: refine hf.fderivWithin' hg ?_ hmn hst
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x₀ : E
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 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
have rw : ∀ᶠ (x : E) in 𝓝[s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
Tactic: rw [insert_eq_self.mpr hx₀]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : 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
⊢ s ⊆ (fun (x : E) ↦ x) ⁻¹' s
have rw : s ⊆ s
Tactic: rw [preimage_id']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
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
⊢ s ⊆ (fun (x : F) ↦ x) ⁻¹' s
have rw : s ⊆ s
Tactic: rw [preimage_id']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
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
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
m : ℕ∞ω
hmn : m + (↑0 : ℕ∞ω) ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 0 f s) s x₀
have hmn₁ : m ≤ n
Tactic: simp only [CharP.cast_eq_zero, add_zero] at hmn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
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
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
i : ℕ
hi :
  ∀ {m : ℕ∞ω} (hmn : m + (↑i : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 i f s) s x₀
m : ℕ∞ω
hmn : m + (↑(i + 1) : ℕ∞ω) ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 (i + 1) f s) s x₀
have hmn₁ : m + 1 + (↑i : ℕ∞ω) ≤ n
Tactic: rw [Nat.cast_succ, add_comm _ 1, ← add_assoc] at hmn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + (↑i : ℕ∞ω) ≤ n
hx₀s : x₀ ∈ s
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 i f s) s x₀
have zero : ∀ {m : ℕ∞ω} (hmn : m + (↑0 : ℕ∞ω) ≤ n),
  ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 0 f s) s x₀
Tactic: induction i generalizing m with
  | zero =>
    simp only [CharP.cast_eq_zero, add_zero] at hmn
    exact (hf.of_le hmn).continuousLinearMap_comp
      ((continuousMultilinearCurryFin0 𝕜 E F).symm : _ →L[𝕜] E [×0]→L[𝕜] F)
  | succ i hi =>
    rw [Nat.cast_succ, add_comm _ 1, ← add_assoc] at hmn
    exact ((hi hmn).fderivWithin_right hs le_rfl hx₀s).continuousLinearMap_comp
      ((continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (i + 1) ↦ E) F).symm :
        _ →L[𝕜] E [×(i + 1)]→L[𝕜] F)
Cleared hypotheses: m, i, hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + (↑i : ℕ∞ω) ≤ n
hx₀s : x₀ ∈ s
zero :
  ∀ {m : ℕ∞ω} (hmn : m + (↑0 : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 0 f s) s x₀
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 i f s) s x₀
have succ : ∀ (i : ℕ)
  (hi :
    ∀ {m : ℕ∞ω} (hmn : m + (↑i : ℕ∞ω) ≤ n),
      ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
        (iteratedFDerivWithin 𝕜 i f s) s x₀)
  {m : ℕ∞ω} (hmn : m + (↑(i + 1) : ℕ∞ω) ≤ n),
  ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 (i + 1) f s) s x₀
Tactic: induction i generalizing m with
  | zero =>
    simp only [CharP.cast_eq_zero, add_zero] at hmn
    exact (hf.of_le hmn).continuousLinearMap_comp
      ((continuousMultilinearCurryFin0 𝕜 E F).symm : _ →L[𝕜] E [×0]→L[𝕜] F)
  | succ i hi =>
    rw [Nat.cast_succ, add_comm _ 1, ← add_assoc] at hmn
    exact ((hi hmn).fderivWithin_right hs le_rfl hx₀s).continuousLinearMap_comp
      ((continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (i + 1) ↦ E) F).symm :
        _ →L[𝕜] E [×(i + 1)]→L[𝕜] F)
Cleared hypotheses: m, i, hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderiv 𝕜 (f x) (g x)) x₀
have simp_rw : ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) univ (g x)) x₀
Tactic: simp_rw [← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) univ (g x)) x₀
have refine : univ ⊆ g ⁻¹' univ
Tactic: refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
    hmn (mem_univ x₀) ?_).contDiffAt univ_mem
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ univ ⊆ g ⁻¹' univ
have rw : Subset.{u_2} (α := Set E) univ univ
Tactic: rw [preimage_univ]