mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case a
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
x : α
s : Set (Set α)
hs : s ∈ (Besicovitch.vitaliFamily μ).filterAt x
ε : ℝ
εpos : ε > 0
hε : ∀ a ∈ (Besicovitch.vitaliFamily μ).setsAt x, a ⊆ closedBall x ε → a ∈ s
_r : ℝ
hr : _r ∈ Ioc 0 ε
⊢ (fun r ↦ closedBall x r) _r ⊆ closedBall x ε

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
x : α
s : Set (Set α)
hs : s ∈ (Besicovitch.vitaliFamily μ).filterAt x
ε : ℝ
εpos : ε > 0
hε : ∀ a ∈ (Besicovitch.vitaliFamily μ).setsAt x, a ⊆ closedBall x ε → a ∈ s
_r : ℝ
hr : _r ∈ Ioc 0 ε
⊢ (fun r ↦ closedBall x r) _r ⊆ closedBall x ε
Module: Mathlib.Analysis.Calculus.FDeriv.Partial

Goal state before:
pp: case cf'
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
this✝ : RCLike 𝕜 := ⋯
h :
  Tendsto (fun x ↦ ((Prod.fst ∘ Prod.fst ∘ Prod.fst) x, x.2)) (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.2)
    (𝓝 u.1 ×ˢ 𝓝 u.2)
this : NormedSpace ℝ E₂ := ⋯
⊢ Tendsto
    (↿fun x y ↦
      match x with
      | (v, w) => f₂ v.1 y)
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.2) (𝓝 (↿f₂ u))

Tactic:
·

Goal state after:
case cf'
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
this✝ : RCLike 𝕜 := ⋯
h :
  Tendsto (fun x ↦ ((Prod.fst ∘ Prod.fst ∘ Prod.fst) x, x.2)) (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.2)
    (𝓝 u.1 ×ˢ 𝓝 u.2)
this : NormedSpace ℝ E₂ := ⋯
⊢ Tendsto
    (↿fun x y ↦
      match x with
      | (v, w) => f₂ v.1 y)
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.2) (𝓝 (↿f₂ u))
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x

Tactic:
obtain rfl | ht := eq_or_ne t 0

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (0 • x)
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (0 • x)
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (0 • x)
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t ↦ |1 + t|) 0 * ‖x‖ = ‖x‖

pp: case hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ |1 + t|) 0

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t ↦ |1 + t|) 0 * ‖x‖ = ‖x‖
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ ↑(SignType.sign (1 + 0)) * 1 * ‖x‖ = ‖x‖

pp: case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

pp: case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ ↑(SignType.sign (1 + 0)) * 1 * ‖x‖ = ‖x‖
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

pp: case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0

Tactic:
·

Goal state after:
case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

Tactic:
· rw [h.hasGradientAt.hasDerivAt.deriv, RCLike.conj_conj]

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0

Tactic:
·

Goal state after:
case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ |1 + t|) 0

Tactic:
·

Goal state after:
case hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ |1 + t|) 0
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Subsingleton E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Subsingleton E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Subsingleton E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
simp_rw [(hasFDerivAt_of_subsingleton _ _).fderiv, smul_zero]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
obtain rfl | ht := eq_or_ne t 0

Goal state after:
case pos.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (0 • x) = ↑(SignType.sign 0) • fderiv ℝ (fun x ↦ ‖x‖) x

case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
ht : t ≠ 0
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case pos.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (0 • x) = ↑(SignType.sign 0) • fderiv ℝ (fun x ↦ ‖x‖) x

pp: case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
ht : t ≠ 0
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case pos.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (0 • x) = ↑(SignType.sign 0) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
ht : t ≠ 0
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
ht : t ≠ 0
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ 0 = ↑(SignType.sign t) • 0

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ 0 = ↑(SignType.sign t) • 0
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ ¬DifferentiableAt ℝ (fun x ↦ ‖x‖) (t • x)
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff

Goal state before:
pp: case hf₀'
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ HasFDerivAt (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑?m.110) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))

pp: case hf
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))

pp: 𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ E ≃L[𝕂] F

Tactic:
·

Goal state after:
case hf₀'
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ HasFDerivAt (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑?m.110) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff

Goal state before:
pp: case hf
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))

Tactic:
·

Goal state after:
case hf
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: case disjoint
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ Disjoint (↑f'u).ker (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂)).ker

pp: case codisjoint
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ Codisjoint (↑f'u).ker (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂)).ker

Tactic:
·

Goal state after:
case disjoint
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ Disjoint (↑f'u).ker (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂)).ker
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: case codisjoint
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ Codisjoint (↑f'u).ker (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂)).ker

Tactic:
·

Goal state after:
case codisjoint
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ Codisjoint (↑f'u).ker (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂)).ker
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace 𝕜
z₀ : 𝕜
R R₁ : 𝕜 → 𝕜
hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z
k : ℕ
IH :
  ∀ {t : ℕ},
    (∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) →
      ∃ R₂,
        (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧
          ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t)! / ↑t ! * R₁ z + (z - z₀) * R₂ z)
t : ℕ
hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + 1 + t) * R₁ z
R₂ : 𝕜 → 𝕜
hR₂ : ∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z
hR₂_eq : ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z)
R₂' : 𝕜 → 𝕜 := fun z ↦ (↑t + 1) * R₂ z + (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))
z : 𝕜
hsub : HasDerivAt (fun x ↦ x - z₀) 1 z
⊢ deriv (fun w ↦ (w - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ w + (w - z₀) * R₂ w)) z =
    (↑t + 1) * (z - z₀) ^ t * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z) +
      (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))

Tactic:
simpa using! ((hsub.fun_pow (t + 1)).mul
          (((hf1 z).differentiableAt.hasDerivAt.const_mul ((k + (t + 1))! / (t + 1)! : 𝕜)).add
            (hsub.mul (hR₂ z).differentiableAt.hasDerivAt))).deriv

Goal state after: