awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ DiffContOnCl 𝕜 f s ↔ DifferentiableOn 𝕜 f s

Tactic:
⟨fun h => h.differentiableOn, fun h => ⟨h, hs.closure_eq.symm ▸ h.continuousOn⟩⟩

Premises used: DiffContOnCl.mk, DifferentiableOn.continuousOn, IsClosed.closure_eq, Eq.rec, Iff.intro, DiffContOnCl.differentiableOn, Eq.symm
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
⊢ DiffContOnCl 𝕜 f univ ↔ Differentiable 𝕜 f

Tactic:
isClosed_univ.diffContOnCl_iff.trans differentiableOn_univ

Premises used: isClosed_univ, differentiableOn_univ, IsClosed.diffContOnCl_iff, Iff.trans
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
c : F
⊢ DiffContOnCl.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c) s

Tactic:
⟨differentiableOn_const c, continuousOn_const⟩

Premises used: DiffContOnCl.mk, continuousOn_const, differentiableOn_const
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : G → E
t : Set G
hf : DiffContOnCl 𝕜 f s
hg : DiffContOnCl 𝕜 g t
h : MapsTo g t s
⊢ DiffContOnCl 𝕜 (f ∘ g) t

Tactic:
⟨hf.1.comp hg.1 h, hf.2.comp hg.2 <| h.closure_of_continuousOn hg.2⟩

Premises used: DiffContOnCl.mk, ContinuousOn.comp, DiffContOnCl.continuousOn, DiffContOnCl.differentiableOn, DifferentiableOn.comp, Set.MapsTo.closure_of_continuousOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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)
inl : ∀ (h : DiffContOnCl 𝕜 f (ball x 0)), ContinuousOn f (closedBall x 0)
inr : ∀ (hr : r ≠ 0), ContinuousOn f (closedBall x r)
⊢ ContinuousOn f (closedBall x r)

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
h : DiffContOnCl 𝕜 f (ball x 0)
inl : ContinuousOn f {x}
⊢ ContinuousOn f (closedBall x 0)

Tactic:
rw [closedBall_zero]

Premises used: Metric.closedBall_zero
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
continuousOn_singleton f x

Premises used: continuousOn_singleton
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
exact continuousOn_singleton f x

Premises used: continuousOn_singleton
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
inr : ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))
⊢ ContinuousOn f (closedBall x r)

Tactic:
rw [← closure_ball x hr]

Premises used: closure_ball
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))

Tactic:
h.continuousOn

Premises used: DiffContOnCl.continuousOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))

Tactic:
exact h.continuousOn

Premises used: DiffContOnCl.continuousOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
x : E
r : ℝ
hd : DifferentiableOn 𝕜 f (ball x r)
hc : ContinuousOn f (closedBall x r)
⊢ DiffContOnCl 𝕜 f (ball x r)

Tactic:
⟨hd, hc.mono <| closure_ball_subset_closedBall⟩

Premises used: DiffContOnCl.mk, Metric.closure_ball_subset_closedBall, ContinuousOn.mono
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
x : E
h : DiffContOnCl 𝕜 f s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hx : x ∈ s
⊢ DifferentiableAt 𝕜 f x

Tactic:
h.differentiableOn.differentiableAt <| hs.mem_nhds hx

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
x : E
h : DiffContOnCl 𝕜 f s
hx : s ∈ 𝓝 x
⊢ DifferentiableAt 𝕜 f x

Tactic:
h.differentiableOn.differentiableAt hx

Premises used: DifferentiableOn.differentiableAt, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s t : Set E
h : DiffContOnCl 𝕜 f s
ht : t ⊆ s
⊢ DiffContOnCl 𝕜 f t

Tactic:
⟨h.differentiableOn.mono ht, h.continuousOn.mono (closure_mono ht)⟩

Premises used: DiffContOnCl.mk, closure_mono, DiffContOnCl.continuousOn, ContinuousOn.mono, DifferentiableOn.mono, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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 g : E → F
s : Set E
hf : DiffContOnCl 𝕜 f s
hg : DiffContOnCl 𝕜 g s
⊢ DiffContOnCl 𝕜 (f + g) s

Tactic:
⟨hf.1.add hg.1, hf.2.add hg.2⟩

Premises used: DiffContOnCl.mk, DiffContOnCl.continuousOn, DifferentiableOn.add, ContinuousOn.add, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
hf : DiffContOnCl 𝕜 f s
c : F
⊢ DiffContOnCl.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f x + c) s

Tactic:
hf.add diffContOnCl_const

Premises used: diffContOnCl_const, DiffContOnCl.add
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
hf : DiffContOnCl 𝕜 f s
c : F
⊢ DiffContOnCl.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c + f x) s

Tactic:
diffContOnCl_const.add hf

Premises used: diffContOnCl_const, DiffContOnCl.add
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
hf : DiffContOnCl 𝕜 f s
⊢ DiffContOnCl 𝕜 (-f) s

Tactic:
⟨hf.1.neg, hf.2.neg⟩

Premises used: DiffContOnCl.mk, ContinuousOn.neg, DifferentiableOn.neg, DiffContOnCl.continuousOn, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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 g : E → F
s : Set E
hf : DiffContOnCl 𝕜 f s
hg : DiffContOnCl 𝕜 g s
⊢ DiffContOnCl 𝕜 (f - g) s

Tactic:
⟨hf.1.sub hg.1, hf.2.sub hg.2⟩

Premises used: DiffContOnCl.mk, DifferentiableOn.sub, ContinuousOn.sub, DiffContOnCl.continuousOn, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
hf : DiffContOnCl 𝕜 f s
c : F
⊢ DiffContOnCl.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f x - c) s

Tactic:
hf.sub diffContOnCl_const

Premises used: diffContOnCl_const, DiffContOnCl.sub
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
hf : DiffContOnCl 𝕜 f s
c : F
⊢ DiffContOnCl.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c - f x) s

Tactic:
diffContOnCl_const.sub hf

Premises used: diffContOnCl_const, DiffContOnCl.sub
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
s : Set E
R : Type u_5
inst_5 : Semiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
hf : DiffContOnCl 𝕜 f s
c : R
⊢ DiffContOnCl 𝕜 (c • f) s

Tactic:
⟨hf.1.const_smul c, hf.2.const_smul c⟩

Premises used: DiffContOnCl.mk, DiffContOnCl.continuousOn, DifferentiableOn.const_smul, DiffContOnCl.differentiableOn, ContinuousOn.const_smul
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
𝕜' : Type u_5
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' F
inst_8 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
f : E → F
s : Set E
hc : DiffContOnCl 𝕜 c s
hf : DiffContOnCl 𝕜 f s
⊢ DiffContOnCl.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c x • f x) s

Tactic:
⟨hc.1.smul hf.1, hc.2.smul hf.2⟩

Premises used: DiffContOnCl.mk, DiffContOnCl.continuousOn, DifferentiableOn.smul, ContinuousOn.smul, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
𝕜' : Type u_5
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' F
inst_8 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
s : Set E
hc : DiffContOnCl 𝕜 c s
y : F
⊢ DiffContOnCl.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c x • y) s

Tactic:
hc.smul diffContOnCl_const

Premises used: DiffContOnCl.smul, diffContOnCl_const
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
f : E → 𝕜
hf : DiffContOnCl 𝕜 f s
h₀ : ∀ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, f x ≠ 0
⊢ DiffContOnCl 𝕜 f⁻¹ s

Tactic:
⟨(differentiableOn_inv.comp hf.1 fun _ hx => h₀ _ (subset_closure hx) :), hf.2.inv₀ h₀⟩

Premises used: DiffContOnCl.mk, DiffContOnCl.continuousOn, ContinuousOn.inv₀, DiffContOnCl.differentiableOn, DifferentiableOn.comp
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : G → E
t : Set G
hf : Differentiable 𝕜 f
hg : DiffContOnCl 𝕜 g t
⊢ DiffContOnCl 𝕜 (f ∘ g) t

Tactic:
hf.diffContOnCl.comp hg (mapsTo_image _ _)

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, Set.mapsTo_image
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
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
U : Set E
c : E
R : ℝ
hf : DifferentiableOn 𝕜 f U
hc : closedBall c R ⊆ U
⊢ DiffContOnCl 𝕜 f (ball c R)

Tactic:
DiffContOnCl.mk_ball (hf.mono (ball_subset_closedBall.trans hc)) (hf.continuousOn.mono hc)

Premises used: Metric.ball_subset_closedBall, DifferentiableOn.continuousOn, DiffContOnCl.mk_ball, HasSubset.Subset.trans, ContinuousOn.mono, DifferentiableOn.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
h : ∀ (x : E), extDerivWithin ω univ x = extDeriv ω x
⊢ extDerivWithin ω univ = extDeriv ω

Tactic:
ext1 x
-- 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 : alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = extDeriv ω x
h₁ : alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = alternatizeUncurryFin (fderiv 𝕜 ω x)
h₂ h₃ : alternatizeUncurryFin (fderiv 𝕜 ω x) = alternatizeUncurryFin (fderiv 𝕜 ω x)
⊢ extDerivWithin ω univ x = extDeriv ω x

Tactic:
rw [extDerivWithin, extDeriv, fderivWithin_univ]

Premises used: fderivWithin_univ, extDeriv, 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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
hω₁ : DifferentiableWithinAt 𝕜 ω₁ s x
hω₂ : DifferentiableWithinAt 𝕜 ω₂ s x
⊢ extDerivWithin (ω₁ + ω₂) s x = extDerivWithin ω₁ s x + extDerivWithin ω₂ s x

Tactic:
simp [extDerivWithin, fderivWithin_add hsx hω₁ hω₂, alternatizeUncurryFin_add]

Premises used: extDerivWithin, ContinuousAlternatingMap.alternatizeUncurryFin_add, fderivWithin_add
-- 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
hsx : UniqueDiffWithinAt 𝕜 s x
hω₁ : DifferentiableWithinAt 𝕜 ω₁ s x
hω₂ : DifferentiableWithinAt 𝕜 ω₂ s x
⊢ extDerivWithin (fun (x : E) ↦ ω₁ x + ω₂ x) s x = extDerivWithin ω₁ s x + extDerivWithin ω₂ s x

Tactic:
extDerivWithin_add hsx hω₁ hω₂

Premises used: extDerivWithin_add
-- 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
hω₂ : DifferentiableAt 𝕜 ω₂ x
⊢ extDeriv (ω₁ + ω₂) x = extDeriv ω₁ x + extDeriv ω₂ x

Tactic:
simp [← extDerivWithin_univ, extDerivWithin_add, *, DifferentiableAt.differentiableWithinAt]

Premises used: extDerivWithin_add, DifferentiableAt.differentiableWithinAt, 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ω₁ : DifferentiableAt 𝕜 ω₁ x
hω₂ : DifferentiableAt 𝕜 ω₂ x
⊢ extDeriv (fun (x : E) ↦ ω₁ x + ω₂ x) x = extDeriv ω₁ x + extDeriv ω₂ x

Tactic:
extDeriv_add hω₁ hω₂

Premises used: extDeriv_add
-- 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 : ℕ
s : Set E
x : E
c : 𝕜
ω : E → E [⋀^Fin n]→L[𝕜] F
hsx : UniqueDiffWithinAt 𝕜 s x
simp : alternatizeUncurryFin (fderivWithin 𝕜 (c • ω) s x) = c • alternatizeUncurryFin (fderivWithin 𝕜 ω s x)
⊢ extDerivWithin (c • ω) s x = c • extDerivWithin ω s x

Tactic:
simp [extDerivWithin, fderivWithin_const_smul_field, hsx, alternatizeUncurryFin_smul]

Premises used: ContinuousAlternatingMap.alternatizeUncurryFin_smul, fderivWithin_const_smul_field, 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 : ℕ
s : Set E
x : E
c : 𝕜
ω : E → E [⋀^Fin n]→L[𝕜] F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ extDerivWithin (fun (x : E) ↦ c • ω x) s x = c • extDerivWithin ω s x

Tactic:
extDerivWithin_smul c ω hsx

Premises used: extDerivWithin_smul
-- 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 : ℕ
x : E
c : 𝕜
ω : E → E [⋀^Fin n]→L[𝕜] F
⊢ extDeriv (c • ω) x = c • extDeriv ω x

Tactic:
simp [← extDerivWithin_univ, extDerivWithin_smul]

Premises used: extDerivWithin_univ, extDerivWithin_smul
-- 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 : ℕ
x : E
c : 𝕜
ω : E → E [⋀^Fin n]→L[𝕜] F
⊢ extDeriv (c • ω) x = c • extDeriv ω x

Tactic:
extDeriv_smul c ω

Premises used: extDeriv_smul
-- 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
s : Set E
x : E
f : E → F
hs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E [⋀^Fin (HAdd.hAdd (α := ℕ) 0 1)]→L[𝕜] F)
    (extDerivWithin (fun (x : E) ↦ constOfIsEmpty 𝕜 E (Fin 0) (f x)) s x)
    ((ofSubsingleton 𝕜 E F 0 : (a : E →L[𝕜] F) → E [⋀^Fin 1]→L[𝕜] F) (fderivWithin 𝕜 f s x))

Tactic:
simp only [extDerivWithin, ← constOfIsEmptyLIE_apply, ← Function.comp_def _ f,
    (constOfIsEmptyLIE 𝕜 E F (Fin 0)).comp_fderivWithin hs,
    alternatizeUncurryFin_constOfIsEmptyLIE_comp]

Premises used: LinearIsometryEquiv.comp_fderivWithin, ContinuousAlternatingMap.constOfIsEmptyLIE_apply, ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp, Function.comp_def, extDerivWithin, ContinuousAlternatingMap.constOfIsEmptyLIE, OfNat.ofNat, Fin
-- 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
f : E → F
x : E
⊢ Eq (α := E [⋀^Fin (HAdd.hAdd (α := ℕ) 0 1)]→L[𝕜] F) (extDeriv (fun (x : E) ↦ constOfIsEmpty 𝕜 E (Fin 0) (f x)) x)
    ((ofSubsingleton 𝕜 E F 0 : (a : E →L[𝕜] F) → E [⋀^Fin 1]→L[𝕜] F) (fderiv 𝕜 f x))

Tactic:
simp [← extDerivWithin_univ, extDerivWithin_constOfIsEmpty, fderivWithin_univ]

Premises used: extDerivWithin_constOfIsEmpty, fderivWithin_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
s : Set E
x : E
hs : ω₁ =ᶠ[𝓝[s] x] ω₂
hx : ω₁ x = ω₂ x
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

Tactic:
simp only [extDerivWithin, alternatizeUncurryFin, hs.fderivWithin_eq hx]

Premises used: Filter.EventuallyEq.fderivWithin_eq, ContinuousAlternatingMap.alternatizeUncurryFin, 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
s : Set E
x : E
hs : ω₁ =ᶠ[𝓝[s] x] ω₂
hx : x ∈ s
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

Tactic:
hs.extDerivWithin_eq (mem_of_mem_nhdsWithin hx hs :)

Premises used: mem_of_mem_nhdsWithin, 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 : ω₁ =ᶠ[𝓝[insert x s] x] ω₂
apply : ω₁ x = ω₂ x
⊢ extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

Tactic:
apply Filter.EventuallyEq.extDerivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)

Premises used: Filter.EventuallyEq.extDerivWithin_eq, Set.subset_insert, 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 : ω₁ =ᶠ[𝓝[insert x s] x] ω₂
⊢ ω₁ x = ω₂ x

Tactic:
(mem_of_mem_nhdsWithin (mem_insert x s) hs :)

Premises used: Set.Mem, setOf, mem_of_mem_nhdsWithin, Set.mem_insert
-- 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 : ω₁ =ᶠ[𝓝[insert x s] x] ω₂
⊢ ω₁ x = ω₂ x

Tactic:
exact (mem_of_mem_nhdsWithin (mem_insert x s) hs :)

Premises used: mem_of_mem_nhdsWithin, Set.mem_insert