awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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)
have 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)
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)]
Cleared hypotheses: i, hi, x, hx, m
-- 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
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) ((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)
have 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)
Tactic: simp only [← iteratedFDerivWithin_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
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₀)
have refine : (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
Tactic: refine nhdsWithin_mono _ ?_ (nhdsWithin_prod self_mem_nhdsWithin 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
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₀
⊢ (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
have simp_rw : s ⊆ (fun (x : E) ↦ (x, g x)) ⁻¹' 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]
-- 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₀
simp_rw : s ⊆ (fun (x : E) ↦ (x, g x)) ⁻¹' insert x₀ s ×ˢ (g '' s)
⊢ (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
have simp_rw₁ : s ⊆ (fun (x : E) ↦ x) ⁻¹' insert x₀ s ∩ g ⁻¹' g '' s
Tactic: simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]
-- 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₀
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
⊢ (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
have simp_rw₂ : s ⊆ insert x₀ s ∩ g ⁻¹' g '' s
Tactic: simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]
-- 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₀
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
⊢ (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
have simp_rw₃ : s ⊆ insert x₀ s ∧ s ⊆ g ⁻¹' g '' s
Tactic: simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]
-- 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₀
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
⊢ (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
have simp_rw₄ : True ∧ s ⊆ g ⁻¹' g '' s
Tactic: simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]
-- 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₀
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
⊢ (fun (x : E) ↦ (x, g x)) '' s ⊆ insert x₀ s ×ˢ (g '' s)
have simp_rw₅ : s ⊆ g ⁻¹' g '' s
Tactic: simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]
-- 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₀
⊢ ∃ 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₀
have hst : 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]
-- 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 ∈ 𝓝[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₀
have 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₀
Tactic: obtain ⟨v, hv, hvs, f_an, f', hvf', hf'⟩ :=
    (contDiffWithinAt_succ_iff_hasFDerivWithinAt' hn).mp hf
-- 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₀)
⊢ ∃ 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₀
have refine_1 : (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s ∈ 𝓝[insert 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), ?_, ?_⟩
-- 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₀)
refine_1 : (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s ∈ 𝓝[insert 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₀
have 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)
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), ?_, ?_⟩
-- 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₀)
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)
⊢ ∃ 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₀
have 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₀
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), ?_, ?_⟩
-- 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₀)
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s ∈ 𝓝[insert x₀ s] x₀
have refine_1 : (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[insert x₀ s] x₀
Tactic: refine inter_mem ?_ self_mem_nhdsWithin
-- 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₀)
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[insert x₀ s] x₀
have this : (x₀, g x₀) ∈ v
Tactic: have := mem_of_mem_nhdsWithin (mem_insert _ _) hv
-- 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₀)
this : (x₀, g x₀) ∈ v
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[insert x₀ s] x₀
have refine_1 : (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[s] x₀
Tactic: refine mem_nhdsWithin_insert.mpr ⟨this, ?_⟩
-- 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₀)
this : (x₀, g x₀) ∈ v
⊢ (fun (z : E) ↦ (z, g z)) ⁻¹' v ∈ 𝓝[s] x₀
have refine_1 : v ∈ 𝓝[(fun (x : E) ↦ (id x, g x)) '' s] (id x₀, g x₀)
Tactic: refine (continuousWithinAt_id.prodMk hg.continuousWithinAt).preimage_mem_nhdsWithin' ?_
-- 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₀)
this : (x₀, g x₀) ∈ v
⊢ v ∈ 𝓝[(fun (x : E) ↦ (id x, g x)) '' s] (id x₀, g x₀)
have 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₀)
Tactic: rw [← nhdsWithin_le_iff] at hst hv ⊢
Cleared hypotheses: hst, v, hv, hvs, f_an, f', hvf', hf', this