mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑0) f
x✝¹ : E
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 (fun z ↦ f (a • z)) x✝¹) x✝ = (a ^ 0 • iteratedFDeriv 𝕜 0 f (a • x✝¹)) x✝

Tactic:
;

Goal state after:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑0) f
x✝¹ : E
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 (fun z ↦ f (a • z)) x✝¹) x✝ = (a ^ 0 • iteratedFDeriv 𝕜 0 f (a • x✝¹)) x✝
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
f : 𝕜 → F
s : 𝕜
n : ℕ
IH : (iteratedDeriv n fun z ↦ f (z + s)) = fun t ↦ iteratedDeriv n f (t + s)
⊢ (iteratedDeriv (n + 1) fun z ↦ f (z + s)) = fun t ↦ iteratedDeriv (n + 1) f (t + s)

Tactic:
simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n) (f i) s x) →
    iteratedDerivWithin n (∑ i ∈ t, f i) s x = ∑ i ∈ t, iteratedDerivWithin n (f i) s x
hf : ∀ i_1 ∈ insert i t, ContDiffWithinAt 𝕜 (↑n) (f i_1) s x
⊢ iteratedDerivWithin n (∑ i ∈ insert i t, f i) s x = ∑ i ∈ insert i t, iteratedDerivWithin n (f i) s x

Tactic:
rw [forall_mem_insert] at hf

Goal state after:
case insert
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n) (f i) s x) →
    iteratedDerivWithin n (∑ i ∈ t, f i) s x = ∑ i ∈ t, iteratedDerivWithin n (f i) s x
hf : ContDiffWithinAt 𝕜 (↑n) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n) (f x_1) s x
⊢ iteratedDerivWithin n (∑ i ∈ insert i t, f i) s x = ∑ i ∈ insert i t, iteratedDerivWithin n (f i) s x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ∞ω
𝕜' : Type u_4
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ∀ (x : E), ContDiffAt 𝕜 n f⁻¹ x

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ∞ω
𝕜' : Type u_4
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ∀ (x : E), ContDiffAt 𝕜 n f⁻¹ x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x ↦ (g b - g a) * f x - (f b - f a) * g x
⊢ (g b - g a) * f a - (f b - f a) * g a = (g b - g a) * f b - (f b - f a) * g b

Tactic:
;

Goal state after:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x ↦ (g b - g a) * f x - (f b - f a) * g x
⊢ (g b - g a) * f a - (f b - f a) * g a = (g b - g a) * f b - (f b - f a) * g b
Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus

Goal state before:
pp: X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s i)) =ᶠ[li] m
this : (fun s ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b) =o[l.smallSets] fun s ↦ μ.real s
a : ι
ha : μ.real (s a) = m a
⊢ ∫ (x : X) in s a, f x ∂μ - μ.real (s a) • b = ∫ (x : X) in s a, f x ∂μ - m a • b

Tactic:
;

Goal state after:
X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s i)) =ᶠ[li] m
this : (fun s ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b) =o[l.smallSets] fun s ↦ μ.real s
a : ι
ha : μ.real (s a) = m a
⊢ ∫ (x : X) in s a, f x ∂μ - μ.real (s a) • b = ∫ (x : X) in s a, f x ∂μ - m a • b
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case pos.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : c = 0
⊢ ∫⁻ (x : α), ↑((fun x ↦ 0) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
· simp only [lintegral_const, zero_mul, zero_le, ENNReal.coe_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((eapproxDiff f n) x) ∂μ + δ n
n : ℕ
⊢ AEMeasurable (fun x ↦ ↑((eapproxDiff f n) x)) μ

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((eapproxDiff f n) x) ∂μ + δ n
n : ℕ
⊢ AEMeasurable (fun x ↦ ↑((eapproxDiff f n) x)) μ
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < f' x

Tactic:
;

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x

Tactic:
;

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f' x

Tactic:
;

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x

Tactic:
;

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ f' x < 0

Tactic:
;

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ f' x < 0
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0

Tactic:
;

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ f' x ≤ 0

Tactic:
;

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ f' x ≤ 0
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0

Tactic:
;

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case mk
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
C C₁ C₂✝ : ConvexCone R M
s : Set M
c : R
x : M
C₂ : ConvexCone R M
carrier✝ : Set M
smul_mem'✝ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier✝ → c • x ∈ carrier✝
add_mem'✝ : ∀ ⦃x : M⦄, x ∈ carrier✝ → ∀ ⦃y : M⦄, y ∈ carrier✝ → x + y ∈ carrier✝
h : { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ }.carrier = C₂.carrier
⊢ { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ } = C₂

Tactic:
;

Goal state after:
case mk
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
C C₁ C₂✝ : ConvexCone R M
s : Set M
c : R
x : M
C₂ : ConvexCone R M
carrier✝ : Set M
smul_mem'✝ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier✝ → c • x ∈ carrier✝
add_mem'✝ : ∀ ⦃x : M⦄, x ∈ carrier✝ → ∀ ⦃y : M⦄, y ∈ carrier✝ → x + y ∈ carrier✝
h : { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ }.carrier = C₂.carrier
⊢ { carrier := carrier✝, smul_mem' := smul_mem'✝, add_mem' := add_mem'✝ } = C₂
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
C : ConvexCone R M
⊢ ↑C = ↑⊥ ↔ C = ⊥

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
C : ConvexCone R M
⊢ ↑C = ↑⊥ ↔ C = ⊥
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : sᶜ ⊆ {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
⊢ f x = AEMeasurable.mk f fmeas x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : sᶜ ⊆ {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
⊢ f x = AEMeasurable.mk f fmeas x
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ‖f z - f y - ((fderiv 𝕜 f x) z - (fderiv 𝕜 f x) y)‖ =
    ‖f z - f x - ((fderiv 𝕜 f x) z - (fderiv 𝕜 f x) x) - (f y - f x - ((fderiv 𝕜 f x) y - (fderiv 𝕜 f x) x))‖

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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ‖f z - f y - ((fderiv 𝕜 f x) z - (fderiv 𝕜 f x) y)‖ =
    ‖f z - f x - ((fderiv 𝕜 f x) z - (fderiv 𝕜 f x) x) - (f y - f x - ((fderiv 𝕜 f x) y - (fderiv 𝕜 f x) x))‖
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
C : ConvexCone R M
⊢ C.Pointed ↔ ¬C.Blunt

Tactic:
simp [Blunt, Pointed]

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

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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : ‖y - x‖ < r
z : E
hz : ‖z - x‖ < r
⊢ δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r

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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : ‖y - x‖ < r
z : E
hz : ‖z - x‖ < r
⊢ δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
x : G
⊢ 0 ∈ C

Tactic:
;

Goal state after:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
x : G
⊢ 0 ∈ C
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case ha
𝕜 : 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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ⋯
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ 0 < r

pp: case hbc
𝕜 : 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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ⋯
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ε / 2 < ε

Tactic:
;

Goal state after:
case ha
𝕜 : 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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ⋯
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ 0 < r

case hbc
𝕜 : 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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ⋯
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ε / 2 < ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case e'_8
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y

Tactic:
;

Goal state after:
case e'_8
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x : M
x✝¹ : ConvexCone R M
x✝ : M
⊢ x✝ ∈ 0 + x✝¹ ↔ x✝ ∈ x✝¹

Tactic:
;

Goal state after:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x : M
x✝¹ : ConvexCone R M
x✝ : M
⊢ x✝ ∈ 0 + x✝¹ ↔ x✝ ∈ x✝¹
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x : M
x✝¹ : ConvexCone R M
x✝ : M
⊢ x✝ ∈ x✝¹ + 0 ↔ x✝ ∈ x✝¹

Tactic:
;

Goal state after:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x : M
x✝¹ : ConvexCone R M
x✝ : M
⊢ x✝ ∈ x✝¹ + 0 ↔ x✝ ∈ x✝¹
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₁.hy
𝕜 : 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
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ x ∈ closedBall x (r / 2)

Tactic:
simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]

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

Goal state before:
pp: case h₂.hy
𝕜 : 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
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ x ∈ closedBall x (r / 2)

Tactic:
simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
r : 𝕜
hr : 0 < r
y : M
hy : y ∈ s
⊢ (fun x ↦ r • x) y ∈ hull 𝕜 s

Tactic:
;

Goal state after:
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
r : 𝕜
hr : 0 < r
y : M
hy : y ∈ s
⊢ (fun x ↦ r • x) y ∈ hull 𝕜 s
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x✝ : M
⊢ x✝ ∈ ↑(hull 𝕜 s) ↔ x✝ ∈ {x | ∃ r, 0 < r ∧ x ∈ r • s}

Tactic:
;

Goal state after:
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x✝ : M
⊢ x✝ ∈ ↑(hull 𝕜 s) ↔ x✝ ∈ {x | ∃ r, 0 < r ∧ x ∈ r • s}
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ Disjoint ↑(hull 𝕜 s) ↑C → Disjoint s ↑C

Tactic:
;

Goal state after:
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ Disjoint ↑(hull 𝕜 s) ↑C → Disjoint s ↑C
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case refine_1
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 + y ≠ 0 ∧ 1 - y ≠ 0

Tactic:
;

Goal state after:
case refine_1
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 + y ≠ 0 ∧ 1 - y ≠ 0