awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DiffContOnCl (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closedBall x r)
have inr : ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))
Tactic: rw [← closure_ball x hr]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
ω : E → E [⋀^Fin n]→L[𝕜] F
⊢ extDerivWithin ω univ = extDeriv ω
have h : ∀ (x : E), extDerivWithin ω univ x = extDeriv ω x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
⊢ extDerivWithin ω univ x = extDeriv ω x
have h : alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = extDeriv ω x
Tactic: rw [extDerivWithin, extDeriv, fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
h : alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = extDeriv ω x
⊢ extDerivWithin ω univ x = extDeriv ω x
have h₁ : alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = alternatizeUncurryFin (fderiv 𝕜 ω x)
Tactic: rw [extDerivWithin, extDeriv, fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
h : alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = extDeriv ω x
h₁ : alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = alternatizeUncurryFin (fderiv 𝕜 ω x)
⊢ extDerivWithin ω univ x = extDeriv ω x
have h₂ : alternatizeUncurryFin (fderiv 𝕜 ω x) = alternatizeUncurryFin (fderiv 𝕜 ω x)
Tactic: rw [extDerivWithin, extDeriv, fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
s : Set E
x : E
c : 𝕜
ω : E → E [⋀^Fin n]→L[𝕜] F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ extDerivWithin (c • ω) s x = c • extDerivWithin ω s x
have simp : alternatizeUncurryFin (fderivWithin 𝕜 (c • ω) s x) = c • alternatizeUncurryFin (fderivWithin 𝕜 ω s x)
Tactic: simp [extDerivWithin, fderivWithin_const_smul_field, hsx, alternatizeUncurryFin_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hs : ω₁ =ᶠ[𝓝[insert x s] x] ω₂
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x
have apply : ω₁ x = ω₂ x
Tactic: apply Filter.EventuallyEq.extDerivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F
x : E
h : ω₁ =ᶠ[𝓝 x] ω₂
⊢ extDeriv ω₁ =ᶠ[𝓝 x] extDeriv ω₂
have simp : ∀ (h : ω₁ =ᶠ[𝓝[univ] x] ω₂), extDerivWithin ω₁ univ =ᶠ[𝓝[univ] x] extDerivWithin ω₂ univ
Tactic: simp only [← nhdsWithin_univ, ← extDerivWithin_univ] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hω : ContDiffWithinAt 𝕜 r ω s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
⊢ alternatizeUncurryFin (fderivWithin 𝕜 (fun (y : E) ↦ alternatizeUncurryFin (fderivWithin 𝕜 ω s y)) s x) =
    alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL fderivWithin 𝕜 (fderivWithin 𝕜 ω s) s x)
have e_f : Eq (α := E →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] F)
  (fderivWithin 𝕜 (fun (y : E) ↦ alternatizeUncurryFin (fderivWithin 𝕜 ω s y)) s x)
  (alternatizeUncurryFinCLM 𝕜 E F ∘SL fderivWithin 𝕜 (fderivWithin 𝕜 ω s) s x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hω : ContDiffWithinAt 𝕜 r ω s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (fderivWithin 𝕜 ω s) s x
have refine : HAdd.hAdd (α := WithTop ℕ∞) 1 1 ≤ r
Tactic: refine (hω.fderivWithin_right hs ?_ h'x).differentiableWithinAt one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.Basic (hypothesis)
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 : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hω : ContDiffWithinAt 𝕜 r ω s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
⊢ Eq (α := E →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] F)
    (fderivWithin 𝕜 (fun (y : E) ↦ alternatizeUncurryFin (fderivWithin 𝕜 ω s y)) s x)
    (alternatizeUncurryFinCLM 𝕜 E F ∘SL fderivWithin 𝕜 (fderivWithin 𝕜 ω s) s x)
have this : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (fderivWithin 𝕜 ω s) s x
Tactic: have : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 ω s) s x := by
      refine (hω.fderivWithin_right hs ?_ h'x).differentiableWithinAt one_ne_zero
      exact le_minSmoothness.trans hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
hω : ContDiffAt 𝕜 r ω x
hr : minSmoothness 𝕜 2 ≤ r
⊢ extDeriv (extDeriv ω) x = 0
have simp : extDerivWithin (extDerivWithin ω univ) univ x = 0
Tactic: simp only [← extDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
hω : ContDiffAt 𝕜 r ω x
hr : minSmoothness 𝕜 2 ≤ r
⊢ extDerivWithin (extDerivWithin ω univ) univ x = 0
have hs : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ
Tactic: apply extDerivWithin_extDerivWithin_apply (s := univ) hω.contDiffWithinAt hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
hω : ContDiffAt 𝕜 r ω x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ
⊢ extDerivWithin (extDerivWithin ω univ) univ x = 0
have hx : Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)) x
Tactic: apply extDerivWithin_extDerivWithin_apply (s := univ) hω.contDiffWithinAt hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
hω : ContDiffAt 𝕜 r ω x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ
hx : Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)) x
⊢ extDerivWithin (extDerivWithin ω univ) univ x = 0
have h'x : Membership.mem (γ := Set E) univ x
Tactic: apply extDerivWithin_extDerivWithin_apply (s := univ) hω.contDiffWithinAt hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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
n : ℕ
r : WithTop ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x)) s x)
    ((extDerivWithin ω t (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x))
have hdf : DifferentiableWithinAt 𝕜 f s x
Tactic: have hdf : DifferentiableWithinAt 𝕜 f s x :=
    hf.differentiableWithinAt <| (two_pos.trans_le <| le_minSmoothness.trans hr).ne'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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
n : ℕ
r : WithTop ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
hdf : DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x)) s x)
    ((extDerivWithin ω t (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x))
have hd2f : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
Tactic: have hd2f : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f s) s x :=
    (hf.fderivWithin_right hs (le_minSmoothness.trans hr) hxs).differentiableWithinAt one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
hdf : DifferentiableWithinAt 𝕜 f s x
hd2f : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x)) s x)
    ((extDerivWithin ω t (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x))
have rw : Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
  (alternatizeUncurryFin
    (compContinuousLinearMapCLM (fderivWithin 𝕜 f s x) ∘SL fderivWithin 𝕜 ω t (f x) ∘SL fderivWithin 𝕜 f s x))
  ((alternatizeUncurryFin (fderivWithin 𝕜 ω t (f x))).compContinuousLinearMap (fderivWithin 𝕜 f s x))
Tactic: rw [extDerivWithin,
    fderivWithin_continuousAlternatingMapCompContinuousLinearMap (by exact hω.comp x hdf hst) hd2f
      (hs x hxs),
    alternatizeUncurryFin_add, fderivWithin_comp' _ hω hdf hst (hs x hxs), extDerivWithin,
    alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
hdf : DifferentiableWithinAt 𝕜 f s x
hd2f : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
rw :
  Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (alternatizeUncurryFin
      (compContinuousLinearMapCLM (fderivWithin 𝕜 f s x) ∘SL fderivWithin 𝕜 ω t (f x) ∘SL fderivWithin 𝕜 f s x))
    ((alternatizeUncurryFin (fderivWithin 𝕜 ω t (f x))).compContinuousLinearMap (fderivWithin 𝕜 f s x))
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x)) s x)
    ((extDerivWithin ω t (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x))
have hsymm : ∀ (x_1 y : E),
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) x_1 : E →L[𝕜] F) : (a : E) → F) y : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x_1 : F)
Tactic: rw [extDerivWithin,
    fderivWithin_continuousAlternatingMapCompContinuousLinearMap (by exact hω.comp x hdf hst) hd2f
      (hs x hxs),
    alternatizeUncurryFin_add, fderivWithin_comp' _ hω hdf hst (hs x hxs), extDerivWithin,
    alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
hdf : DifferentiableWithinAt 𝕜 f s x
hd2f : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (alternatizeUncurryFin
      (compContinuousLinearMapCLM (fderivWithin 𝕜 f s x) ∘SL fderivWithin 𝕜 ω t (f x) ∘SL fderivWithin 𝕜 f s x))
    ((alternatizeUncurryFin (fderivWithin 𝕜 ω t (f x))).compContinuousLinearMap (fderivWithin 𝕜 f s x))
have H : ∀ (v : Fin (n + 1) → E),
  Eq.{u_4 + 1} (α := G)
    ((alternatizeUncurryFin
            (compContinuousLinearMapCLM (fderivWithin 𝕜 f s x) ∘SL fderivWithin 𝕜 ω t (f x) ∘SL fderivWithin 𝕜 f s x) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)
    (((alternatizeUncurryFin (fderivWithin 𝕜 ω t (f x))).compContinuousLinearMap (fderivWithin 𝕜 f s x) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hω : DifferentiableAt 𝕜 ω (f x)
hf : ContDiffAt 𝕜 r f x
hr : minSmoothness 𝕜 2 ≤ r
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G) (extDeriv (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderiv 𝕜 f x)) x)
    ((extDeriv ω (f x)).compContinuousLinearMap (fderiv 𝕜 f x))
have simp : ∀ (hω : DifferentiableWithinAt 𝕜 ω univ (f x)) (hf : ContDiffWithinAt 𝕜 r f univ x),
  Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)) univ x)
    ((extDerivWithin ω univ (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x))
Tactic: simp only [← differentiableWithinAt_univ, ← extDerivWithin_univ, ← contDiffWithinAt_univ,
    ← fderivWithin_univ] at *
Cleared hypotheses: hω, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
hω₁ : DifferentiableWithinAt 𝕜 ω univ (f x)
hf₁ : ContDiffWithinAt 𝕜 r f univ x
hr₁ : minSmoothness 𝕜 2 ≤ r
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)) univ x)
    ((extDerivWithin ω univ (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x))
have hs : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ
Tactic: apply extDerivWithin_pullback (r := r)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
hω₁ : DifferentiableWithinAt 𝕜 ω univ (f x)
hf₁ : ContDiffWithinAt 𝕜 r f univ x
hr₁ : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)) univ x)
    ((extDerivWithin ω univ (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x))
have hxc : Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)) x
Tactic: apply extDerivWithin_pullback (r := r)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
hω₁ : DifferentiableWithinAt 𝕜 ω univ (f x)
hf₁ : ContDiffWithinAt 𝕜 r f univ x
hr₁ : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ
hxc : Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)) x
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)) univ x)
    ((extDerivWithin ω univ (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x))
have hxs : Membership.mem (γ := Set E) univ x
Tactic: apply extDerivWithin_pullback (r := r)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.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 : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
hω₁ : DifferentiableWithinAt 𝕜 ω univ (f x)
hf₁ : ContDiffWithinAt 𝕜 r f univ x
hr₁ : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ
hxc : Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)) x
hxs : Membership.mem (γ := Set E) univ x
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (extDerivWithin (fun (x : E) ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)) univ x)
    ((extDerivWithin ω univ (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x))
have hst : MapsTo f univ univ
Tactic: apply extDerivWithin_pullback (r := r)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (hypothesis)
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 : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ ((extDerivWithin ω s x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x) =
    HSub.hSub (α := F)
      (∑ i : Fin (n + 2),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                        (i : Fin (n + 1)) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F))
      (∑ i : Fin (n + 1),
        ∑ j ∈ Ici i,
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
            ((ω x : (a : Fin (n + 1) → E) → F)
                (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                    (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E))) :
              F))
have H₀ : ∀ (i : Fin (n + 2)) (j : Fin (n + 1)),
  DifferentiableWithinAt 𝕜 (F := E)
    (fun (y : E) ↦ i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) j) s x
Tactic: have H₀ (i : Fin (n + 2)) (j : Fin (n + 1)) :
      DifferentiableWithinAt 𝕜 (fun y ↦ i.removeNth (V · y) j) s x := hV ..