awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 t : Set E
x : E
hs : ω₁ =ᶠ[𝓝[s] x] ω₂
ht : t ⊆ s
⊢ extDerivWithin ω₁ t =ᶠ[𝓝[s] x] extDerivWithin ω₂ t

Tactic:
(eventually_eventually_nhdsWithin.2 hs).mp <| eventually_mem_nhdsWithin.mono fun _y hys hs =>
    EventuallyEq.extDerivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht)
        (hs.self_of_nhdsWithin hys)

Premises used: Iff.mpr, Filter.Eventually.filter_mono, Filter.Eventually.self_of_nhdsWithin, eventually_mem_nhdsWithin, Filter.EventuallyEq, Filter.Eventually.mono, Filter.Eventually.mp, Filter.EventuallyEq.extDerivWithin_eq, eventually_eventually_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 : ω₁ =ᶠ[𝓝[s] x] ω₂
⊢ extDerivWithin ω₁ s =ᶠ[𝓝[s] x] extDerivWithin ω₂ s

Tactic:
hs.extDerivWithin' .rfl

Premises used: Filter.EventuallyEq.extDerivWithin', Set.Subset.rfl
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
h : ω₁ =ᶠ[𝓝 x] ω₂
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

Tactic:
(h.filter_mono nhdsWithin_le_nhds).extDerivWithin_eq h.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.self_of_nhds, nhdsWithin_le_nhds, Filter.EventuallyEq.extDerivWithin_eq
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 : EqOn ω₁ ω₂ s
hx : ω₁ x = ω₂ x
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

Tactic:
(hs.eventuallyEq.filter_mono inf_le_right).extDerivWithin_eq hx

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Filter.EventuallyEq.extDerivWithin_eq
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 : EqOn ω₁ ω₂ s
hx : x ∈ s
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

Tactic:
extDerivWithin_congr hs (hs hx)

Premises used: extDerivWithin_congr
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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] ω₂
simp : ∀ (h : ω₁ =ᶠ[𝓝[univ] x] ω₂), extDerivWithin ω₁ univ =ᶠ[𝓝[univ] x] extDerivWithin ω₂ univ
⊢ extDeriv ω₁ =ᶠ[𝓝 x] extDeriv ω₂

Tactic:
simp only [← nhdsWithin_univ, ← extDerivWithin_univ] at *

Premises used: nhdsWithin_univ, extDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 : ω₁ =ᶠ[𝓝[univ] x] ω₂
⊢ extDerivWithin ω₁ univ =ᶠ[𝓝[univ] x] extDerivWithin ω₂ univ

Tactic:
h.extDerivWithin

Premises used: Filter.EventuallyEq.extDerivWithin
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 : ω₁ =ᶠ[𝓝[univ] x] ω₂
⊢ extDerivWithin ω₁ univ =ᶠ[𝓝[univ] x] extDerivWithin ω₂ univ

Tactic:
exact h.extDerivWithin

Premises used: Filter.EventuallyEq.extDerivWithin
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 ω₂ x

Tactic:
h.extDeriv.self_of_nhds

Premises used: Filter.Eventually.self_of_nhds, Filter.EventuallyEq.extDeriv
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
h : DifferentiableWithinAt 𝕜 ω s x
hs : UniqueDiffWithinAt 𝕜 s x
v : Fin (n + 1) → E
⊢ Eq.{u_3 + 1} (α := F) ((extDerivWithin ω s x : (a : Fin (n + 1) → E) → F) v : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜 (fun (x : E) ↦ (ω x : (a : Fin n → E) → F) (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v))
                  s x :
                (a : E) → F)
              (v i) :
            F) :
      F)

Tactic:
simp [extDerivWithin, ContinuousAlternatingMap.alternatizeUncurryFin_apply,
    fderivWithin_continuousAlternatingMap_apply_const_apply, *]

Premises used: fderivWithin_continuousAlternatingMap_apply_const_apply, extDerivWithin, ContinuousAlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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 : DifferentiableAt 𝕜 ω x
v : Fin (n + 1) → E
⊢ Eq.{u_3 + 1} (α := F) ((extDeriv ω x : (a : Fin (n + 1) → E) → F) v : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderiv 𝕜 (fun (x : E) ↦ (ω x : (a : Fin n → E) → F) (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v)) x :
                (a : E) → F)
              (v i) :
            F) :
      F)

Tactic:
simp [← extDerivWithin_univ, extDerivWithin_apply h.differentiableWithinAt]

Premises used: DifferentiableAt.differentiableWithinAt, extDerivWithin_univ, extDerivWithin_apply
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
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)
⊢ alternatizeUncurryFin (fderivWithin 𝕜 (fun (y : E) ↦ alternatizeUncurryFin (fderivWithin 𝕜 ω s y)) s x) =
    alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL fderivWithin 𝕜 (fderivWithin 𝕜 ω s) s x)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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

Tactic:
(hω.fderivWithin_right hs ?_ h'x).differentiableWithinAt one_ne_zero

Premises used: one_ne_zero, ContDiffWithinAt.differentiableWithinAt, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
refine : HAdd.hAdd (α := WithTop ℕ∞) 1 1 ≤ r
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (fderivWithin 𝕜 ω s) s x

Tactic:
refine (hω.fderivWithin_right hs ?_ h'x).differentiableWithinAt one_ne_zero

Premises used: one_ne_zero, ContDiffWithinAt.differentiableWithinAt, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ HAdd.hAdd (α := WithTop ℕ∞) 1 1 ≤ r

Tactic:
le_minSmoothness.trans hr

Premises used: le_minSmoothness, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ HAdd.hAdd (α := WithTop ℕ∞) 1 1 ≤ r

Tactic:
exact le_minSmoothness.trans hr

Premises used: le_minSmoothness, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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

Tactic:
have : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 ω s) s x := by
      refine (hω.fderivWithin_right hs ?_ h'x).differentiableWithinAt one_ne_zero
      exact le_minSmoothness.trans hr
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
this : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (fderivWithin 𝕜 ω s) s x
⊢ 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:
alternatizeUncurryFinCLM _ _ _ |>.hasFDerivAt.comp_hasFDerivWithinAt x
      this.hasFDerivWithinAt |>.fderivWithin (hs.uniqueDiffWithinAt h'x)

Premises used: ContinuousLinearMap.hasFDerivAt, UniqueDiffOn.uniqueDiffWithinAt, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.fderivWithin
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
hω : ContDiffOn 𝕜 r ω s
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
x : E
h'x : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
⊢ extDerivWithin (extDerivWithin ω s) s x = 0 x

Tactic:
extDerivWithin_extDerivWithin_apply (hω.contDiffWithinAt h'x) hr hs hx h'x

Premises used: extDerivWithin_extDerivWithin_apply, ContDiffOn.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
hω : ContDiffOn 𝕜 r ω s
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
x : E
h'x : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
⊢ extDerivWithin (extDerivWithin ω s) s x = 0 x

Tactic:
exact extDerivWithin_extDerivWithin_apply (hω.contDiffWithinAt h'x) hr hs hx h'x

Premises used: extDerivWithin_extDerivWithin_apply, ContDiffOn.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
simp : extDerivWithin (extDerivWithin ω univ) univ x = 0
⊢ extDeriv (extDeriv ω) x = 0

Tactic:
simp only [← extDerivWithin_univ]

Premises used: extDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
h'x : Membership.mem (γ := Set E) univ x
⊢ extDerivWithin (extDerivWithin ω univ) univ x = 0

Tactic:
apply extDerivWithin_extDerivWithin_apply (s := univ) hω.contDiffWithinAt hr

Premises used: extDerivWithin_extDerivWithin_apply, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)) x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ Membership.mem (γ := Set E) univ x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
h : ContDiff 𝕜 r ω
hr : minSmoothness 𝕜 2 ≤ r
⊢ extDeriv (extDeriv ω) = 0

Tactic:
funext fun _ ↦ extDeriv_extDeriv_apply h.contDiffAt hr

Premises used: funext, extDeriv_extDeriv_apply, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
have hdf : DifferentiableWithinAt 𝕜 f s x :=
    hf.differentiableWithinAt <| (two_pos.trans_le <| le_minSmoothness.trans hr).ne'
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ 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
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ DifferentiableWithinAt 𝕜 (F := F [⋀^Fin n]→L[𝕜] G) (fun (x : E) ↦ ω (f x)) s x

Tactic:
hω.comp x hdf hst

Premises used: DifferentiableWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
⊢ DifferentiableWithinAt 𝕜 (F := F [⋀^Fin n]→L[𝕜] G) (fun (x : E) ↦ ω (f x)) s x

Tactic:
exact hω.comp x hdf hst

Premises used: DifferentiableWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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))
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)
⊢ 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))

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]

Premises used: fderivWithin_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_comp', extDerivWithin, ContinuousAlternatingMap.alternatizeUncurryFin_add, add_zero, ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic
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
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)
⊢ 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:
ext v