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
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 ∩ U) x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f (s ∩ U) x))
have hfU₁ : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ U)
Tactic: rw [insert_eq_of_mem hx] at hfU
Cleared hypotheses: 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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x)
    (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.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 (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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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))
have zero : ∀ (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)
Tactic: ext1 m
-- 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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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))
have succ : ∀ (m : (i : Fin (i + 1)) → E),
  Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
Tactic: ext1 m
-- 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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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
m : (i : Fin (i + 1)) → E
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
have succ : Eq.{u_4 + 1} (α := G)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
            (m 0) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
        (a : (i : Fin i) → E) → G)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
    G)
  (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
          (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
        (a : (i : Fin (i + 1)) → E) → G)
      m :
    G)
Tactic: rw [iteratedFDerivWithin_succ_apply_left]
-- 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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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
m : (i : Fin (i + 1)) → E
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
have Z : Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
  (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
  (fderivWithin 𝕜
    (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
      (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i f s))
    s x)
Tactic: 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
-- 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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
have succ : Eq.{u_4 + 1} (α := G)
  ((((fderivWithin 𝕜
                (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
                  (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                    (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) →
                      ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
                  (iteratedFDerivWithin 𝕜 i f s))
                s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
            (m 0) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
        (a : (i : Fin i) → E) → G)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
    G)
  (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
          (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
        (a : (i : Fin (i + 1)) → E) → G)
      m :
    G)
Tactic: simp_rw [Z]
-- 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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜
                  (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
                    (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) →
                        ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
                    (iteratedFDerivWithin 𝕜 i f s))
                  s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
have succ : Eq.{u_4 + 1} (α := G)
  (((((↑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G) ∘SL
                fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
            (m 0) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
        (a : (i : Fin i) → E) → G)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
    G)
  (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
          (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
        (a : (i : Fin (i + 1)) → E) → G)
      m :
    G)
Tactic: rw [(g.continuousMultilinearMapCongrRight fun _ : Fin i => E).comp_fderivWithin (hs x 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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
⊢ Eq.{u_4 + 1} (α := G)
    (((((↑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                      ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G) ∘SL
                  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
have succ : Eq.{u_3 + 1} (α := F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F)
            (m 0) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
    F)
  ((iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) m : F)
Tactic: simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
      ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, EmbeddingLike.apply_eq_iff_eq]
-- 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 : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
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
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      F)
    ((iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) m : F)
have succ : Eq.{u_3 + 1} (α := F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F)
            (m 0) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
    F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (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) m) :
    F)
Tactic: rw [iteratedFDerivWithin_succ_apply_left]
-- 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 : ℕ
⊢ 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 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))
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
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))
⊢ 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 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)
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