awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑g : G →L[𝕜] E))
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
m : (i : Fin (i + 1)) → G
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s))
                  ((⇑g : (a : G) → E) ⁻¹' s) x :
                (a : G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ G) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F) :
          (a : (i : Fin i) → G) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ G) m) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
      F)
have this : Eq (α := G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
  (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s))
    ((⇑g : (a : G) → E) ⁻¹' s) x)
  (fderivWithin 𝕜
    (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (_x : Fin i) ↦ E) F)
      (⇑(continuousMultilinearMapCongrLeft (E := fun (_x : Fin i) ↦ G) (E₁ := fun (_x : Fin i) ↦ E) F fun (_x : Fin i) ↦
            g) :
        (a : ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i f s ∘ (⇑g : (a : G) → E)))
    ((⇑g : (a : G) → E) ⁻¹' s) x)
Tactic: have : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
        fderivWithin 𝕜
          (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft _ (fun _x : Fin i => g) ∘
            (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' s) x :=
      fderivWithin_congr' (@IH) hx
-- 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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑g : G →L[𝕜] E))
have zero : ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin 0) ↦ G) F)
    (iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
      (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E))
Tactic: induction i generalizing x with ext1 m
  | zero =>
    simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
  | succ i IH =>
    simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
      ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_succ_apply_left]
    have : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
        fderivWithin 𝕜
          (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft _ (fun _x : Fin i => g) ∘
            (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' s) x :=
      fderivWithin_congr' (@IH) hx
    rw [this, ContinuousLinearEquiv.comp_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]
    simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
      ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
    rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
      ContinuousLinearMap.coe_comp', coe_coe, comp_apply, tail_def, tail_def]
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
s : Set E
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
zero :
  ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin 0) ↦ G) F)
      (iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
        (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑g : G →L[𝕜] E))
have zero₁ : ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)) (m : (i : Fin 0) → G),
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x : (a : (i : Fin 0) → G) → F) m : F)
    ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
            (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E) :
          (a : (i : Fin 0) → G) → F)
        m :
      F)
Tactic: induction i generalizing x with ext1 m
  | zero =>
    simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
  | succ i IH =>
    simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
      ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_succ_apply_left]
    have : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
        fderivWithin 𝕜
          (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft _ (fun _x : Fin i => g) ∘
            (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' s) x :=
      fderivWithin_congr' (@IH) hx
    rw [this, ContinuousLinearEquiv.comp_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]
    simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
      ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
    rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
      ContinuousLinearMap.coe_comp', coe_coe, comp_apply, tail_def, tail_def]
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
n : ℕ∞ω
g : G →L[𝕜] E
f : E → F
hf : ContDiff 𝕜 n f
x : G
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDeriv 𝕜 i (f ∘ (⇑g : (a : G) → E)) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (x : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDeriv 𝕜 i f ((g : (a : G) → E) x)) fun (x : Fin i) ↦ g)
have simp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
  (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) univ x)
  (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (x : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
    (iteratedFDerivWithin 𝕜 i f univ ((g : (a : G) → E) x)) fun (x : Fin i) ↦ g)
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
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
have this : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
  (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
  (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
    (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E))
Tactic: have : iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
      (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g :=
    g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_right 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
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
have rw : norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E)) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
Tactic: rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]
-- 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
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E))
rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
have rw₁ : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
Tactic: rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]
-- 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 : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDeriv 𝕜 i (f ∘ (⇑g : (a : G) → E)) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv 𝕜 i f ((g : (a : G) → E) x))
have simp : norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) univ x) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i f univ ((g : (a : G) → E) x))
Tactic: simp only [← iteratedFDerivWithin_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 : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
      ((e.symm : (a : E) → G) x : G) ↔
    ContDiffWithinAt 𝕜 n f s x
have mp : ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
    ((e.symm : (a : E) → G) x : G) →
  ContDiffWithinAt 𝕜 n f 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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
mp :
  ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
      ((e.symm : (a : E) → G) x : G) →
    ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
      ((e.symm : (a : E) → G) x : G) ↔
    ContDiffWithinAt 𝕜 n f s x
have mpr : ContDiffWithinAt 𝕜 n f s x →
  ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
    ((e.symm : (a : E) → G) x : G)
Tactic: constructor
-- 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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
H : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
    ((e.symm : (a : E) → G) x : G)
have H₁ : ContDiffWithinAt 𝕜 n f s (((↑e : G →L[𝕜] E) : (a : G) → E) ((e.symm : (a : E) → G) x : G))
Tactic: rw [← e.apply_symm_apply x, ← e.coe_coe] at H
Cleared hypotheses: H
-- 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
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((e.symm : (a : E) → G) x : G) ↔
    ContDiffAt 𝕜 n f x
have rw : ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F)
    (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ : Set G) ((e.symm : (a : E) → G) x : G) ↔
  ContDiffWithinAt 𝕜 n f univ x
Tactic: rw [← contDiffWithinAt_univ, ← contDiffWithinAt_univ, ← preimage_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
f : E → F
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
rw :
  ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F)
      (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ : Set G) ((e.symm : (a : E) → G) x : G) ↔
    ContDiffWithinAt 𝕜 n f univ x
rw₁ : Type u_2
⊢ ContDiffAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((e.symm : (a : E) → G) x : G) ↔
    ContDiffAt 𝕜 n f x
have rw₂ : G → E
Tactic: rw [← contDiffWithinAt_univ, ← contDiffWithinAt_univ, ← preimage_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
f : E → F
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiff.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E)) ↔ ContDiff 𝕜 n f
have rw : ContDiffOn.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E))
    (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ) ↔
  ContDiffOn 𝕜 n f univ
Tactic: rw [← contDiffOn_univ, ← contDiffOn_univ, ← preimage_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
f : E → F
n : ℕ∞ω
e : G ≃L[𝕜] E
rw :
  ContDiffOn.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E))
      (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ) ↔
    ContDiffOn 𝕜 n f univ
rw₁ : Type u_2
⊢ ContDiff.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E)) ↔ ContDiff 𝕜 n f
have rw₂ : G → E
Tactic: rw [← contDiffOn_univ, ← contDiffOn_univ, ← preimage_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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := F × G) n (fun (y : E) ↦ (f y, g y))
    (fun (y : E) (k : ℕ) ↦ (p y k).prod (M₁ := fun (i : Fin k) ↦ E) (q y k)) s
have zero_eq : ∀ x ∈ s,
  ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
    (f x, g 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
zero_eq :
  ∀ x ∈ s,
    ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
        (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
      (f x, g x)
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := F × G) n (fun (y : E) ↦ (f y, g y))
    (fun (y : E) (k : ℕ) ↦ (p y k).prod (M₁ := fun (i : Fin k) ↦ E) (q y k)) s
have fderivWithin : ∀ (m : ℕ),
  (↑m : ℕ∞ω) < n →
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
        (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m))
        (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := F × G)
          (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin m.succ) ↦ E) (p x m.succ) (q x m.succ)))
        s x
Tactic: constructor