awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.NormedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
⊢ ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)
have mp : ConformalAt f x → IsConformalMap (fderiv ℝ f x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.NormedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
mp : ConformalAt f x → IsConformalMap (fderiv ℝ f x)
⊢ ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)
have mpr : IsConformalMap (fderiv ℝ f x) → ConformalAt f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.NormedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
⊢ ConformalAt f x
have pos : ∀ (h : DifferentiableAt ℝ f x), ConformalAt f x
Tactic: by_cases h : DifferentiableAt ℝ f x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.NormedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
pos : ∀ (h : DifferentiableAt ℝ f x), ConformalAt f x
⊢ ConformalAt f x
have neg : ∀ (h : ¬DifferentiableAt ℝ f x), ConformalAt f x
Tactic: by_cases h : DifferentiableAt ℝ f x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.NormedSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
⊢ ConformalAt f x
have a : Nontrivial X
Tactic: nontriviality X
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.NormedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedAddCommGroup Z
inst_3 : NormedSpace ℝ X
inst_4 : NormedSpace ℝ Y
inst_5 : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
hf : ConformalAt f x
⊢ ConformalAt (g ∘ f) x
have rcases : ∀ (f' : X →L[ℝ] Y) (hf₁ : HasFDerivAt f f' x) (cf : IsConformalMap f'), ConformalAt (g ∘ f) x
Tactic: rcases hf with ⟨f', hf₁, cf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.NormedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedAddCommGroup Z
inst_3 : NormedSpace ℝ X
inst_4 : NormedSpace ℝ Y
inst_5 : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
⊢ ConformalAt (g ∘ f) x
have rcases : ∀ (g' : Y →L[ℝ] Z) (hg₁ : HasFDerivAt g g' (f x)) (cg : IsConformalMap g'), ConformalAt (g ∘ f) x
Tactic: rcases hg with ⟨g', hg₁, cg⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
c : F
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s) 0
have zero : ∀ (x : E),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s x) (0 x)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
c : F
n : ℕ
IH :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1 + 1) (fun (x : E) ↦ c) s) 0
have succ : Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F)
  (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F) :
      (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F)
    (fderivWithin 𝕜 0 s))
  0
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ
c : F
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0
have zero : Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
  (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s) 0
Tactic: induction n with
  | zero =>
    ext1
    simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
    simp only [Pi.zero_def, comp_def, fderivWithin_fun_const, map_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ
c : F
zero :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0
have succ : ∀ (n : ℕ)
  (IH :
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0),
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1 + 1) (fun (x : E) ↦ c) s) 0
Tactic: induction n with
  | zero =>
    ext1
    simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
    simp only [Pi.zero_def, comp_def, fderivWithin_fun_const, map_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 0 s) 0
have zero : ∀ (x : E) (x_1 : (i : Fin 0) → E),
  Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 0 s x : (a : (i : Fin 0) → E) → F) x_1 : F)
    ((0 x : (a : (i : Fin 0) → E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
i : ℕ
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i 0 s) 0
have zero : Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 0 s) 0
Tactic: cases i with
  | zero => ext; simp
  | succ i => apply iteratedFDerivWithin_succ_const
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
i : ℕ
zero :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 0 s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i 0 s) 0
have succ : ∀ (i : ℕ),
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (i + 1) 0 s) 0
Tactic: cases i with
  | zero => ext; simp
  | succ i => apply iteratedFDerivWithin_succ_const
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
⊢ Eq (α := (s : Set E) → (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 0) 0
have h : ∀ (x : Set E) (x_1 : E) (n : ℕ) (x_2 : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F) ((ftaylorSeriesWithin 𝕜 0 x x_1 n : (a : (i : Fin n) → E) → F) x_2 : F)
    ((0 x x_1 n : (a : (i : Fin n) → E) → F) x_2 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
⊢ Eq (α := (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 0) 0
have h : ∀ (x : E) (n : ℕ) (x_1 : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F) ((ftaylorSeries 𝕜 0 x n : (a : (i : Fin n) → E) → F) x_1 : F)
    ((0 x n : (a : (i : Fin n) → E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
⊢ Eq (α := (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 fun (x : E) ↦ 0) 0
have h : ∀ (x : E) (n : ℕ) (x_1 : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F) ((ftaylorSeries 𝕜 (fun (x : E) ↦ 0) x n : (a : (i : Fin n) → E) → F) x_1 : F)
    ((0 x n : (a : (i : Fin n) → E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiff 𝕜 n f
have rw : ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) n fun (x : E) ↦ 0
Tactic: rw [Subsingleton.elim f fun _ => 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
x : E
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffAt 𝕜 n f x
have rw : ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) x
Tactic: rw [Subsingleton.elim f fun _ => 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffWithinAt 𝕜 n f s x
have rw : ContDiffWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s x
Tactic: rw [Subsingleton.elim f fun _ => 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffOn 𝕜 n f s
have rw : ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s
Tactic: rw [Subsingleton.elim f fun _ => 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ
hn : n ≠ 0
c : F
s : Set E
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ c) s) 0
have zero : ∀ (hn : Ne (α := ℕ) 0 0),
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 (fun (x : E) ↦ c) s) 0
Tactic: cases n with
  | zero => contradiction
  | succ n => exact iteratedFDerivWithin_succ_const n c
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ
hn : n ≠ 0
c : F
s : Set E
zero :
  ∀ (hn : Ne (α := ℕ) 0 0),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (iteratedFDerivWithin 𝕜 0 (fun (x : E) ↦ c) s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ c) s) 0
have succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0),
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0
Tactic: cases n with
  | zero => contradiction
  | succ n => exact iteratedFDerivWithin_succ_const n c
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 ω f s x
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ω ((⇑g : (a : F) → G) ∘ f) s x
have obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p u)
  (h'p :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
        u),
  ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ω ((⇑g : (a : F) → G) ∘ f) s x
Tactic: obtain ⟨u, hu, p, hp, h'p⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ω ((⇑g : (a : F) → G) ∘ f) s x
have refine : ∀ (i : ℕ),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fun (x : E) ↦ g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (p x i)) u
Tactic: refine ⟨u, hu, _, hp.continuousLinearMap_comp g, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fun (x : E) ↦ g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (p x i)) u
have change : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
  (fun (x : E) ↦
    (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
              (a : F →L[𝕜] G) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
            g :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
      (p x i))
  u
Tactic: change AnalyticOn 𝕜
      (fun x ↦ (ContinuousLinearMap.compContinuousMultilinearMapL 𝕜
      (fun _ : Fin i ↦ E) F G g) (p x i)) u
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
    (fun (x : E) ↦
      (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
                (a : F →L[𝕜] G) →
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
              g :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (p x i))
    u
have apply : AnalyticOnNhd 𝕜 (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (F :=
  ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
  (⇑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
            (a : F →L[𝕜] G) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
          g :
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
          ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
    (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
  univ
Tactic: apply AnalyticOnNhd.comp_analyticOn _ (h'p i) (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
x : E
n_1 : ℕ∞ω
g : F →L[𝕜] G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E G), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) ((⇑g : (a : F) → G) ∘ f) p u
have rcases : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
  (hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E G), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) ((⇑g : (a : F) → G) ∘ f) p u
Tactic: rcases hf m hm with ⟨u, hu, p, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
have rcases : ∀ (U : Set E) (hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hxU : x ∈ U)
  (hfU : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (insert x s ∩ U)),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
Tactic: rcases hf.contDiffOn' hi (by simp) with ⟨U, hU, hxU, hfU⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (insert x s ∩ U)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
  (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) (s ∩ U) x)
  (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f (s ∩ U) x))
Tactic: rw [← iteratedFDerivWithin_inter_open hU hxU, ← iteratedFDerivWithin_inter_open (f := f) hU hxU]