awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
zero :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin 0) ↦ E) G)
      (iteratedFDerivWithin 𝕜 0 ((⇑g : (a : F) → G) ∘ f) s x)
      ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ E) (iteratedFDerivWithin 𝕜 0 f s x))
zero₁ :
  ∀ {x : E} (hx : x ∈ s) (m : (i : Fin 0) → E),
    Eq.{u_4 + 1} (α := G) ((iteratedFDerivWithin 𝕜 0 ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin 0) → E) → G) m : G)
      (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ E) (iteratedFDerivWithin 𝕜 0 f s x) :
            (a : (i : Fin 0) → E) → G)
          m :
        G)
⊢ 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 : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
have succ : ∀ (i : ℕ)
  (IH :
    ∀ {x : E} (hx : x ∈ s),
      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 : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)))
  {x : E} (hx : x ∈ s),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin (i + 1)) ↦ E) G)
    (iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
      (iteratedFDerivWithin 𝕜 (i + 1) f s x))
Tactic: induction i generalizing x with ext1 m
  | zero =>
    simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, coe_coe]
  | succ i IH =>
    rw [iteratedFDerivWithin_succ_apply_left]
    have Z : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (g ∘ f) s) s x =
        fderivWithin 𝕜 (g.continuousMultilinearMapCongrRight (fun _ : Fin i => E) ∘
          iteratedFDerivWithin 𝕜 i f s) s x :=
      fderivWithin_congr' (@IH) hx
    simp_rw [Z]
    rw [(g.continuousMultilinearMapCongrRight fun _ : Fin i => E).comp_fderivWithin (hs x hx)]
    simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
      ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, EmbeddingLike.apply_eq_iff_eq]
    rw [iteratedFDerivWithin_succ_apply_left]
Cleared hypotheses: x, hx, 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
f : E → F
x : E
g : F ≃L[𝕜] G
i : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv 𝕜 i f x))
have simp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
  (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x)
  ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f univ x))
Tactic: simp only [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
have this : 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.toContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
Tactic: have :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
    g.toContinuousLinearMap.iteratedFDerivWithin_comp_left hf hs hx hi
-- 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 →ₗᵢ[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
this :
  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.toContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
have rw : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (g.toContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s x)) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
Tactic: rw [this]
-- 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
x : E
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x)
have simp : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f univ x)
Tactic: simp only [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
g : F ≃ₗᵢ[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
have this : 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 : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
    (iteratedFDerivWithin 𝕜 i f s x))
Tactic: have :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      (g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
    g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_left f hs hx 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
x : E
g : F ≃ₗᵢ[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
this :
  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 : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s x))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
have rw : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    ((↑(↑g : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s x)) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
Tactic: rw [this]
-- 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
g : F ≃ₗᵢ[𝕜] G
f : E → F
x : E
i : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x)
have rw : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f univ x)
Tactic: rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
⊢ HasFTaylorSeriesUpToOn.{u_1, u_4, u_3} (𝕜 := 𝕜) n (f ∘ (⇑g : (a : G) → E))
    (fun (x : G) (k : ℕ) ↦
      (p ((g : (a : G) → E) x) k).compContinuousLinearMap (M₁ := fun (i : Fin k) ↦ G) (M₁' := fun (i : Fin k) ↦ E)
        fun (x : Fin k) ↦ g.contLinear)
    ((⇑g : (a : G) → E) ⁻¹' s)
have hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
Tactic: have hA : ∀ m, IsBoundedLinearMap 𝕜 (A m) := fun m =>
    isBoundedLinearMap_continuousMultilinearMap_comp_linear g.contLinear
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
⊢ HasFTaylorSeriesUpToOn.{u_1, u_4, u_3} (𝕜 := 𝕜) n (f ∘ (⇑g : (a : G) → E))
    (fun (x : G) (k : ℕ) ↦
      (p ((g : (a : G) → E) x) k).compContinuousLinearMap (M₁ := fun (i : Fin k) ↦ G) (M₁' := fun (i : Fin k) ↦ E)
        fun (x : Fin k) ↦ g.contLinear)
    ((⇑g : (a : G) → E) ⁻¹' s)
have zero_eq : ∀ (x : G),
  Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x →
    ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
        (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
          (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
      (f ∘ (⇑g : (a : G) → E)) x
Tactic: constructor
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
zero_eq :
  ∀ (x : G),
    Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x →
      ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
          (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
            (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
        (f ∘ (⇑g : (a : G) → E)) x
⊢ HasFTaylorSeriesUpToOn.{u_1, u_4, u_3} (𝕜 := 𝕜) n (f ∘ (⇑g : (a : G) → E))
    (fun (x : G) (k : ℕ) ↦
      (p ((g : (a : G) → E) x) k).compContinuousLinearMap (M₁ := fun (i : Fin k) ↦ G) (M₁' := fun (i : Fin k) ↦ E)
        fun (x : Fin k) ↦ g.contLinear)
    ((⇑g : (a : G) → E) ⁻¹' s)
have fderivWithin : ∀ (m : ℕ),
  (↑m : ℕ∞ω) < n →
    ∀ (x : G),
      Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x →
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
          (fun (x : G) ↦
            (p ((g : (a : G) → E) x) m).compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E)
              fun (x : Fin m) ↦ g.contLinear)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ G)
            (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin m.succ) ↦ G) (M₁' :=
              fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) fun (x : Fin m.succ) ↦ g.contLinear))
          ((⇑g : (a : G) → E) ⁻¹' s) x
Tactic: constructor
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
zero_eq :
  ∀ (x : G),
    Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x →
      ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
          (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
            (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
        (f ∘ (⇑g : (a : G) → E)) x
fderivWithin :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : G),
        Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x →
          HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
            (fun (x : G) ↦
              (p ((g : (a : G) → E) x) m).compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦
                E) fun (x : Fin m) ↦ g.contLinear)
            (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ G)
              (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin m.succ) ↦ G) (M₁' :=
                fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) fun (x : Fin m.succ) ↦ g.contLinear))
            ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ HasFTaylorSeriesUpToOn.{u_1, u_4, u_3} (𝕜 := 𝕜) n (f ∘ (⇑g : (a : G) → E))
    (fun (x : G) (k : ℕ) ↦
      (p ((g : (a : G) → E) x) k).compContinuousLinearMap (M₁ := fun (i : Fin k) ↦ G) (M₁' := fun (i : Fin k) ↦ E)
        fun (x : Fin k) ↦ g.contLinear)
    ((⇑g : (a : G) → E) ⁻¹' s)
have cont : ∀ (m : ℕ),
  (↑m : ℕ∞ω) ≤ n →
    ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
      (fun (x : G) ↦
        (p ((g : (a : G) → E) x) m).compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E)
          fun (x : Fin m) ↦ g.contLinear)
      ((⇑g : (a : G) → E) ⁻¹' s)
Tactic: constructor
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
        (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
    (f ∘ (⇑g : (a : G) → E)) x
have zero_eq : ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
      (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
  ContinuousMultilinearMap.curry0 (p ((g : (a : G) → E) x) 0)
Tactic: simp only [(hf.zero_eq (g x) hx).symm, Function.comp_apply]
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
        (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
    ContinuousMultilinearMap.curry0 (p ((g : (a : G) → E) x) 0)
have zero_eq : Eq.{u_3 + 1} (α := F)
  ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ (g.contLinear : (a : G) → E) 0 : F)
  ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) 0 : F)
Tactic: change (p (g x) 0 fun _ : Fin 0 => g.contLinear 0) = p (g x) 0 0
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ Eq.{u_3 + 1} (α := F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ (g.contLinear : (a : G) → E) 0 : F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) 0 : F)
have zero_eq : Eq.{u_3 + 1} (α := F) ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
  ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) 0 : F)
Tactic: rw [map_zero]