mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h ↦ h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h ↦ h ^ 2
this : (fun h ↦ 1 / h ^ 2) =O[𝓝[>] 0] fun h ↦ 1 / h ^ 2
C : (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x ↦ (1 / x ^ 2) • x ^ 2
⊢ (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =ᶠ[𝓝[>] 0] fun x ↦ (f'' w) v - (f'' v) w

pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h ↦ h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h ↦ h ^ 2
this : (fun h ↦ 1 / h ^ 2) =O[𝓝[>] 0] fun h ↦ 1 / h ^ 2
C : (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x ↦ (1 / x ^ 2) • x ^ 2
⊢ (fun x ↦ (1 / x ^ 2) • x ^ 2) =ᶠ[𝓝[>] 0] fun x ↦ 1

Tactic:
·

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h ↦ h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h ↦ h ^ 2
this : (fun h ↦ 1 / h ^ 2) =O[𝓝[>] 0] fun h ↦ 1 / h ^ 2
C : (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x ↦ (1 / x ^ 2) • x ^ 2
⊢ (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =ᶠ[𝓝[>] 0] fun x ↦ (f'' w) v - (f'' v) w
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
A : ∑' (x : ↑t0), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε / 2
B : ∀ (i : Fin N), ∑' (x : ↑(Subtype.val '' S i)), μ (closedBall (↑x) (r ↑x)) ≤ ε / 2 / ↑N
⊢ μ s + ε / 2 + ∑ i, ε / 2 / ↑N ≤ μ s + ε / 2 + ε / 2

Tactic:
by
        gcongr
        simp only [Finset.card_fin, Finset.sum_const, nsmul_eq_mul, ENNReal.mul_div_le]

Goal state after:
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
⊢ lineDeriv 𝕜 f x (0 • v) = 0 • lineDeriv 𝕜 f x v

pp: case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
⊢ lineDeriv 𝕜 f x (0 • v) = 0 • lineDeriv 𝕜 f x v
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : ¬LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : ¬LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : ¬LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h ↦ h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h ↦ h ^ 2
this : (fun h ↦ 1 / h ^ 2) =O[𝓝[>] 0] fun h ↦ 1 / h ^ 2
C : (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x ↦ (1 / x ^ 2) • x ^ 2
⊢ (fun x ↦ (1 / x ^ 2) • x ^ 2) =ᶠ[𝓝[>] 0] fun x ↦ 1

Tactic:
·

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h ↦ h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h ↦ h ^ 2
this : (fun h ↦ 1 / h ^ 2) =O[𝓝[>] 0] fun h ↦ 1 / h ^ 2
C : (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x ↦ (1 / x ^ 2) • x ^ 2
⊢ (fun x ↦ (1 / x ^ 2) • x ^ 2) =ᶠ[𝓝[>] 0] fun x ↦ 1
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case pos.hu
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ W (f y)) s x

Tactic:
·

Goal state after:
case pos.hu
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ W (f y)) s x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
⊢ pullbackWithin 𝕜 f V u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f V s

pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
⊢ pullbackWithin 𝕜 f W u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f W s

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
⊢ pullbackWithin 𝕜 f V u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f V s
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
⊢ pullbackWithin 𝕜 f W u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f W s

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
⊢ pullbackWithin 𝕜 f W u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f W s
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 : ContDiffAt ℝ 0 (fun x ↦ ‖x‖) (t • x)
⊢ ContDiffAt ℝ 0 (fun x ↦ ‖x‖) x

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (t • x)
hn : n ≠ 0
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : ContDiffAt ℝ 0 (fun x ↦ ‖x‖) (t • x)
⊢ ContDiffAt ℝ 0 (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
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (t • x)
hn : n ≠ 0
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x

Tactic:
obtain rfl | ht := eq_or_ne t 0

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (0 • x)
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x

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

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (0 • x)
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x

pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (t • x)
hn : n ≠ 0
ht : t ≠ 0
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (0 • x)
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (t • x)
hn : n ≠ 0
ht : t ≠ 0
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x

Tactic:
·

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (t • x)
hn : n ≠ 0
ht : t ≠ 0
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : r ≤ δ / 2
⊢ (g x ∩ Ioo 0 δ).Nonempty

pp: case inr
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : r ≤ δ / 2
⊢ (g x ∩ Ioo 0 δ).Nonempty
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
⊢ (g x ∩ Ioo 0 δ).Nonempty
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = |t| * ‖t⁻¹ • x✝‖

pp: case e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
e_8✝ : instAddCommGroup = normedAddCommGroup.toAddCommGroup
e_9✝ : Semiring.toModule ≍ RCLike.toInnerProductSpaceReal.toModule
⊢ ↑(SignType.sign t) • f = (|t| • f) ∘SL (t⁻¹ • ContinuousLinearMap.id ℝ E)

Tactic:
·

Goal state after:
case e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = |t| * ‖t⁻¹ • x✝‖
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞