awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x
⊢ f = star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
⊢ HasDerivAt (𝕜 := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → F) (star (star f'))
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) : 𝕜)

Tactic:
hf.star_conj

Premises used: HasDerivAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
h : f' = star (star f')
h₁ : x = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
⊢ HasDerivAt (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x

Tactic:
convert! hf.star_conj

Premises used: HasDerivAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
⊢ f' = star (star f')

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
⊢ x = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
x : 𝕜
inst_2 : NormedStarGroup 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAt f f' x
⊢ HasDerivAt (𝕜 := 𝕜) (F := 𝕜) ((⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) f' : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
hf.star_conj

Premises used: HasDerivAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NormedStarGroup 𝕜
f : 𝕜 → 𝕜
x f' : 𝕜
⊢ HasDerivAt ((⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x ↔
    HasDerivAt f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)

Tactic:
hasDerivAt_star_conj_iff

Premises used: hasDerivAt_star_conj_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (E := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → F)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
hf.star_star

Premises used: DifferentiableAt.star_star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) x
⊢ DifferentiableAt 𝕜 (E := 𝕜)
    (star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) :
      𝕜 → F)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
hf.star_conj

Premises used: DifferentiableAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) x
h : f = star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)
⊢ DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)

Tactic:
convert! hf.star_conj

Premises used: DifferentiableAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) x
⊢ f = star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
⊢ DifferentiableAt 𝕜 (E := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → F)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) : 𝕜)

Tactic:
hf.star_conj

Premises used: DifferentiableAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
h : x = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
⊢ DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) x

Tactic:
convert! hf.star_conj

Premises used: DifferentiableAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
⊢ x = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
x : 𝕜
inst_2 : NormedStarGroup 𝕜
f : 𝕜 → 𝕜
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (E := 𝕜) (F := 𝕜) ((⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
hf.star_star

Premises used: DifferentiableAt.star_star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
x : 𝕜
inst_2 : NormedStarGroup 𝕜
f : 𝕜 → 𝕜
⊢ DifferentiableAt 𝕜 (F := 𝕜) ((⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) x ↔
    DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)

Tactic:
differentiableAt_star_conj_iff

Premises used: differentiableAt_star_conj_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
h :
  ∀ (z : 𝕜),
    deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
⊢ Eq (α := (x : 𝕜) → F) (deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)))
    (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜))

Tactic:
ext z
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
pos :
  ∀ (hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)),
    deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
neg :
  ∀ (hf : ¬DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)),
    deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
⊢ deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z

Tactic:
by_cases hf : DifferentiableAt 𝕜 f (conj z)

Premises used: DifferentiableAt, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)
⊢ deriv (𝕜 := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → F)
      ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) : 𝕜) =
    star (deriv f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z))

Tactic:
hf.hasDerivAt.star_conj.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)
h : z = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
⊢ deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z

Tactic:
convert! hf.hasDerivAt.star_conj.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)
⊢ z = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
hf : ¬DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)
⊢ ¬DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z

Tactic:
have := differentiableAt_star_conj_iff.not.2 hf
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
hf : ¬DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)
this : ¬DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
⊢ deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z

Tactic:
simp_all [deriv_zero_of_not_differentiableAt]

Premises used: deriv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NormedStarGroup 𝕜
f : 𝕜 → 𝕜
⊢ Eq (α := (x : 𝕜) → 𝕜) (deriv ((⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)))
    ((⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜))

Tactic:
deriv_star_conj

Premises used: deriv_star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : x ∉ tsupport f
⊢ f =ᶠ[nhds x] 0

Tactic:
rw [notMem_tsupport_iff_eventuallyEq] at h

Premises used: notMem_tsupport_iff_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ HasStrictDerivAt f 0 x

Tactic:
(hasStrictDerivAt_const x 0).congr_of_eventuallyEq h.symm

Premises used: hasStrictDerivAt_const, OfNat.ofNat, HasStrictDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ HasStrictDerivAt f 0 x

Tactic:
exact (hasStrictDerivAt_const x 0).congr_of_eventuallyEq h.symm

Premises used: hasStrictDerivAt_const, OfNat.ofNat, HasStrictDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : x ∉ tsupport f
⊢ HasDerivAt f 0 x

Tactic:
(HasStrictDerivAt.of_notMem_tsupport h).hasDerivAt

Premises used: HasStrictDerivAt.of_notMem_tsupport, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
s : Set 𝕜
h : x ∉ tsupport f
⊢ HasDerivWithinAt f 0 s x

Tactic:
(HasDerivAt.of_notMem_tsupport h).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivAt.of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ deriv f x = 0

Tactic:
simp [h.deriv_eq]

Premises used: Filter.EventuallyEq.deriv_eq
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
rw : x ∉ tsupport f → deriv f x = 0
⊢ x ∈ support (deriv f) → x ∈ tsupport f

Tactic:
rw [← not_imp_not, notMem_support]

Premises used: Function.notMem_support, not_imp_not
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∉ tsupport f → deriv f x = 0

Tactic:
deriv_of_notMem_tsupport

Premises used: deriv_of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∉ tsupport f → deriv f x = 0

Tactic:
exact deriv_of_notMem_tsupport

Premises used: deriv_of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ tsupport (deriv f) ⊆ tsupport f

Tactic:
closure_minimal support_deriv_subset isClosed_closure

Premises used: closure_minimal, tsupport, support_deriv_subset, isClosed_closure
-- Module: Mathlib.Analysis.Calculus.Deriv.Support
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
hf : HasCompactSupport f
⊢ HasCompactSupport (deriv f)

Tactic:
hf.mono' support_deriv_subset

Premises used: HasCompactSupport.mono', support_deriv_subset
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℤ
hm : 0 < m
⊢ 0 ≤ m

Tactic:
hm.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℤ
hm : 0 < m
lift :
  ∀ (m : ℕ) (hm : LT.lt (α := ℤ) 0 (↑m : ℤ)),
    HasStrictDerivAt (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑m : ℤ)) ((↑(↑m : ℤ) : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1)
      x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x

Tactic:
lift m to ℕ using hm.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
simp : HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑m : ℤ)) ((↑(↑m : ℤ) : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1) x

Tactic:
simp only [zpow_natCast, Int.cast_natCast]

Premises used: zpow_natCast, Int.cast_natCast
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x

Tactic:
hasStrictDerivAt_pow m x

Premises used: hasStrictDerivAt_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
h₁ : x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1 = x ^ (m - 1)
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1) x

Tactic:
convert! hasStrictDerivAt_pow m x using 2

Premises used: hasStrictDerivAt_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
h₁ : 1 ≤ m
⊢ x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1 = x ^ (m - 1)

Tactic:
rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_sub, Int.ofNat_one
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
h₁ h₂ h₃ h₄ : ∀ (hm : 0 < m), 1 ≤ m
⊢ 1 ≤ m

Tactic:
norm_cast at hm
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
⊢ ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x

Tactic:
have : ∀ m : ℤ, 0 < m → HasStrictDerivAt (· ^ m) ((m : 𝕜) * x ^ (m - 1)) x := fun m hm ↦ by
    lift m to ℕ using hm.le
    simp only [zpow_natCast, Int.cast_natCast]
    convert! hasStrictDerivAt_pow m x using 2
    rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]
    norm_cast at hm
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
inl : ∀ (hm : m < 0), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
inr : ∀ (hm : m = 0), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
inr₁ : ∀ (hm : 0 < m), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x

Tactic:
rcases lt_trichotomy m 0 with (hm | hm | hm)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := h.resolve_right hm.not_ge
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
inl :
  ∀
    (this :
      HasStrictDerivAt (Inv.inv ∘ fun (x : 𝕜) ↦ x ^ (-m))
        (((↑(-m) : 𝕜) * x ^ (-m - 1)) • -(HPow.hPow (β := ℕ) (x ^ (-m)) 2)⁻¹) x),
    HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
inl₁ : x ^ (-m) ≠ 0
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x

Tactic:
have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm))
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ x ^ (-m) ≠ 0

Tactic:
zpow_ne_zero _ hx

Premises used: zpow_ne_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ x ^ (-m) ≠ 0

Tactic:
exact zpow_ne_zero _ hx

Premises used: zpow_ne_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ HasStrictDerivAt (Inv.inv ∘ fun (x : 𝕜) ↦ x ^ (-m))
    (((↑(-m) : 𝕜) * x ^ (-m - 1)) • -(HPow.hPow (β := ℕ) (x ^ (-m)) 2)⁻¹) x

Tactic:
have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm)) <;>
      [skip; exact zpow_ne_zero _ hx]

Premises used: zpow_ne_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this_1 : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this :
  HasStrictDerivAt (Inv.inv ∘ fun (x : 𝕜) ↦ x ^ (-m))
    (((↑(-m) : 𝕜) * x ^ (-m - 1)) • -(HPow.hPow (β := ℕ) (x ^ (-m)) 2)⁻¹) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x

Tactic:
simp only [Function.comp_def, zpow_neg, inv_inv, smul_eq_mul] at this

Premises used: Function.comp_def, inv_inv, zpow_neg, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this_1 : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x

Tactic:
this
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this_1 : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x
h₁ : (↑m : 𝕜) * x ^ (m - 1) = (↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x

Tactic:
convert! this using 1