awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜' f s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' f s x)) (fderivWithin 𝕜 f s x)

Tactic:
((hf.hasFDerivWithinAt.restrictScalars 𝕜).fderivWithin hs).symm

Premises used: HasFDerivWithinAt.restrictScalars, HasFDerivWithinAt.fderivWithin, Eq.symm, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
mp :
  DifferentiableWithinAt 𝕜' f s x →
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)
mpr :
  (∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)) →
    DifferentiableWithinAt 𝕜' f s x
⊢ DifferentiableWithinAt 𝕜' f s x ↔
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
g' : E →L[𝕜'] F
hg' : HasFDerivWithinAt f g' s x
⊢ ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)

Tactic:
⟨g', hs.eq (hg'.restrictScalars 𝕜) hf.hasFDerivWithinAt⟩

Premises used: HasFDerivWithinAt.restrictScalars, Exists.intro, DifferentiableWithinAt.hasFDerivWithinAt, UniqueDiffWithinAt.eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
g' : E →L[𝕜'] F
hg' : HasFDerivWithinAt f g' s x
⊢ ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)

Tactic:
exact ⟨g', hs.eq (hg'.restrictScalars 𝕜) hf.hasFDerivWithinAt⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
f' : E →L[𝕜'] F
hf' : Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 f') (fderivWithin 𝕜 f s x)
⊢ DifferentiableWithinAt 𝕜' f s x

Tactic:
⟨f', hf.hasFDerivWithinAt.of_restrictScalars 𝕜 hf'⟩

Premises used: Exists.intro, DifferentiableWithinAt, HasFDerivWithinAt.of_restrictScalars, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
f' : E →L[𝕜'] F
hf' : Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 f') (fderivWithin 𝕜 f s x)
⊢ DifferentiableWithinAt 𝕜' f s x

Tactic:
exact ⟨f', hf.hasFDerivWithinAt.of_restrictScalars 𝕜 hf'⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
rw :
  DifferentiableWithinAt 𝕜' f univ x ↔
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f univ x)
⊢ DifferentiableAt 𝕜' f x ↔ ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderiv 𝕜 f x)

Tactic:
rw [← differentiableWithinAt_univ, ← fderivWithin_univ]

Premises used: fderivWithin_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableWithinAt 𝕜' f univ x ↔
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f univ x)

Tactic:
differentiableWithinAt_iff_restrictScalars 𝕜 hf.differentiableWithinAt uniqueDiffWithinAt_univ

Premises used: DifferentiableAt.differentiableWithinAt, differentiableWithinAt_iff_restrictScalars, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableWithinAt 𝕜' f univ x ↔
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f univ x)

Tactic:
exact
    differentiableWithinAt_iff_restrictScalars 𝕜 hf.differentiableWithinAt uniqueDiffWithinAt_univ

Premises used: DifferentiableAt.differentiableWithinAt, differentiableWithinAt_iff_restrictScalars, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
inst_9 : TrivialStar 𝕜
h : HasFDerivAtFilter f f' L
⊢ HasFDerivAtFilter (fun (x : E) ↦ star (f x)) ((↑(starL' 𝕜) : F →L[𝕜] F) ∘SL f') L

Tactic:
(starL' 𝕜 : F ≃L[𝕜] F).toContinuousLinearMap.hasFDerivAtFilter.comp h Filter.tendsto_map

Premises used: ContinuousLinearMap.hasFDerivAtFilter, HasFDerivAtFilter.comp, Filter.tendsto_map, starL', ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
f' : E →L[𝕜] F
x : E
inst_9 : TrivialStar 𝕜
h : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ star (f x)) ((↑(starL' 𝕜) : F →L[𝕜] F) ∘SL f') x

Tactic:
HasFDerivAtFilter.star h

Premises used: HasFDerivAtFilter.star, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_9 : TrivialStar 𝕜
h : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ star (f x)) ((↑(starL' 𝕜) : F →L[𝕜] F) ∘SL f') s x

Tactic:
HasFDerivAtFilter.star h

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.star
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
f' : E →L[𝕜] F
x : E
inst_9 : TrivialStar 𝕜
h : HasFDerivAt f f' x
⊢ HasFDerivAt (fun (x : E) ↦ star (f x)) ((↑(starL' 𝕜) : F →L[𝕜] F) ∘SL f') x

Tactic:
HasFDerivAtFilter.star h

Premises used: HasFDerivAt, HasFDerivAtFilter.star
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
x : E
s : Set E
inst_9 : TrivialStar 𝕜
h : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ star (f y)) s x

Tactic:
h.hasFDerivWithinAt.star.differentiableWithinAt

Premises used: HasFDerivWithinAt.star, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
x : E
s : Set E
inst_9 : TrivialStar 𝕜
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ star (f y)) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
(starL' 𝕜 : F ≃L[𝕜] F).comp_differentiableWithinAt_iff

Premises used: starL', ContinuousLinearEquiv.comp_differentiableWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
x : E
inst_9 : TrivialStar 𝕜
h : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ star (f y)) x

Tactic:
h.hasFDerivAt.star.differentiableAt

Premises used: HasFDerivAt.star, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
x : E
inst_9 : TrivialStar 𝕜
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ star (f y)) x ↔ DifferentiableAt 𝕜 f x

Tactic:
(starL' 𝕜 : F ≃L[𝕜] F).comp_differentiableAt_iff

Premises used: starL', ContinuousLinearEquiv.comp_differentiableAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
s : Set E
inst_9 : TrivialStar 𝕜
h : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ star (f y)) s

Tactic:
fun x hx => (h x hx).star

Premises used: DifferentiableOn, DifferentiableWithinAt.star
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
s : Set E
inst_9 : TrivialStar 𝕜
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ star (f y)) s ↔ DifferentiableOn 𝕜 f s

Tactic:
(starL' 𝕜 : F ≃L[𝕜] F).comp_differentiableOn_iff

Premises used: ContinuousLinearEquiv.comp_differentiableOn_iff, starL'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
inst_9 : TrivialStar 𝕜
h : Differentiable 𝕜 f
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (y : E) ↦ star (f y)

Tactic:
fun x => (h x).star

Premises used: Differentiable, DifferentiableAt.star
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
inst_9 : TrivialStar 𝕜
⊢ (Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (y : E) ↦ star (f y)) ↔ Differentiable 𝕜 f

Tactic:
(starL' 𝕜 : F ≃L[𝕜] F).comp_differentiable_iff

Premises used: starL', ContinuousLinearEquiv.comp_differentiable_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
x : E
s : Set E
inst_9 : TrivialStar 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ star (f y)) s x)
    ((↑(starL' 𝕜) : F →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)

Tactic:
(starL' 𝕜 : F ≃L[𝕜] F).comp_fderivWithin hxs

Premises used: starL', ContinuousLinearEquiv.comp_fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
f : E → F
x : E
inst_9 : TrivialStar 𝕜
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ star (f y)) x) ((↑(starL' 𝕜) : F →L[𝕜] F) ∘SL fderiv 𝕜 f x)

Tactic:
(starL' 𝕜 : F ≃L[𝕜] F).comp_fderiv

Premises used: ContinuousLinearEquiv.comp_fderiv, starL'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
inst_9 : StarAddMonoid E
inst_10 : StarModule 𝕜 E
inst_11 : ContinuousStar E
inst_12 : NormedStarGroup 𝕜
f : E → F
z : E
f' : E →L[𝕜] F
hf : HasFDerivAt f f' z
⊢ HasFDerivAt f f' (((↑(starL 𝕜) : E →L⋆[𝕜] E) : (a : E) → E) (star z))

Tactic:
simpa using hf
-- Module: Mathlib.Analysis.Calculus.FDeriv.Star
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : StarAddMonoid F
inst_6 : NormedSpace 𝕜 F
inst_7 : StarModule 𝕜 F
inst_8 : ContinuousStar F
inst_9 : StarAddMonoid E
inst_10 : StarModule 𝕜 E
inst_11 : ContinuousStar E
inst_12 : NormedStarGroup 𝕜
f : E → F
z : E
hf : DifferentiableAt 𝕜 f z
⊢ DifferentiableAt 𝕜 (star ∘ f ∘ star) (star z)

Tactic:
hf.hasFDerivAt.star_star.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.star_star
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
v w : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
h v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : IsSymmSndFDerivAt 𝕜 f x
v w : E
⊢ Eq.{u_3 + 1} (α := F) ((((fderiv 𝕜 (fderiv 𝕜 f) x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderiv 𝕜 (fderiv 𝕜 f) x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
h v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ Ne (α := ℕ∞ω) 2 ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y

Tactic:
have : ∀ᶠ y in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y :=
      nhdsWithin_le_iff.2 h (nhdsWithin_mono _ (subset_insert x t) (hf.eventually (by simp)))
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
h₁ :
  ∀ (y : E) (hy : y ∈ s) (h'y : ContDiffWithinAt 𝕜 2 f t y) (h''y : ∀ᶠ (x : E) in 𝓝[s] y, t x),
    Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
⊢ ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)

Tactic:
filter_upwards [self_mem_nhdsWithin, this, eventually_eventually_nhdsWithin.2 h]
      with y hy h'y h''y

Premises used: Iff.mpr, self_mem_nhdsWithin, eventually_eventually_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
y : E
hy : y ∈ s
h'y : ContDiffWithinAt 𝕜 2 f t y
h''y : ∀ᶠ (x : E) in 𝓝[s] y, t x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)

Tactic:
fderivWithin_of_mem_nhdsWithin h''y (hs y hy) (h'y.differentiableWithinAt two_ne_zero)

Premises used: fderivWithin_of_mem_nhdsWithin, two_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
y : E
hy : y ∈ s
h'y : ContDiffWithinAt 𝕜 2 f t y
h''y : ∀ᶠ (x : E) in 𝓝[s] y, t x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)

Tactic:
exact fderivWithin_of_mem_nhdsWithin h''y (hs y hy) (h'y.differentiableWithinAt two_ne_zero)

Premises used: fderivWithin_of_mem_nhdsWithin, two_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)

Tactic:
have A : ∀ᶠ y in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y := by
    have : ∀ᶠ y in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y :=
      nhdsWithin_le_iff.2 h (nhdsWithin_mono _ (subset_insert x t) (hf.eventually (by simp)))
    filter_upwards [self_mem_nhdsWithin, this, eventually_eventually_nhdsWithin.2 h]
      with y hy h'y h''y
    exact fderivWithin_of_mem_nhdsWithin h''y (hs y hy) (h'y.differentiableWithinAt two_ne_zero)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
apply : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x)

Tactic:
apply Filter.EventuallyEq.fderivWithin_eq A

Premises used: Filter.EventuallyEq.fderivWithin_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
fderivWithin_of_mem_nhdsWithin h (hs x hx) (hf.differentiableWithinAt two_ne_zero)

Premises used: fderivWithin_of_mem_nhdsWithin, two_ne_zero, ContDiffWithinAt.differentiableWithinAt