mathlib-initiative/mathlib-tactics huggingface dataset:
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)

pp: case h₁.hz
𝕜 : 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 + y ∈ closedBall x (r / 2)

Tactic:
·

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case hf₀'
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ HasDerivAt (↑expPartialHomeomorph) y (↑expPartialHomeomorph.symm y)

pp: case hf
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph) (↑expPartialHomeomorph.symm y)

Tactic:
·

Goal state after:
case hf₀'
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ HasDerivAt (↑expPartialHomeomorph) y (↑expPartialHomeomorph.symm y)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₁.hz
𝕜 : 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 + y ∈ closedBall x (r / 2)

Tactic:
·

Goal state after:
case h₁.hz
𝕜 : 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 + y ∈ closedBall x (r / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case hf
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph) (↑expPartialHomeomorph.symm y)

Tactic:
·

Goal state after:
case hf
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph) (↑expPartialHomeomorph.symm y)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₂
𝕜 : 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
⊢ ‖f (x + y) - f x - L₁ (x + y - x)‖ ≤ ε * r

Tactic:
·

Goal state after:
case h₂
𝕜 : 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
⊢ ‖f (x + y) - f x - L₁ (x + y - x)‖ ≤ ε * r
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case inl
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log x

pp: case inr
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : 0 < x
⊢ ContDiffAt ℝ n log x

Tactic:
·

Goal state after:
case inl
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log 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)

pp: case h₂.hz
𝕜 : 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 + y ∈ closedBall x (r / 2)

Tactic:
·

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case hg
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log (-x)

pp: case hf
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (fun y ↦ -y) x

Tactic:
·

Goal state after:
case hg
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log (-x)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₂.hz
𝕜 : 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 + y ∈ closedBall x (r / 2)

Tactic:
·

Goal state after:
case h₂.hz
𝕜 : 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 + y ∈ closedBall x (r / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case inr
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : 0 < x
⊢ ContDiffAt ℝ n log x

Tactic:
·

Goal state after:
case inr
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : 0 < x
⊢ ContDiffAt ℝ n log x
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : r < 0
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

pp: case inr.inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = 0 • (y - z)

pp: case inr.inr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
·

Goal state after:
case inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : r < 0
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case inr.inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = 0 • (y - z)

pp: case inr.inr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
·

Goal state after:
case inr.inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = 0 • (y - z)
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case inr.inr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
·

Goal state after:
case inr.inr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ Integrable (fun x ↦ (g x).toReal) μ

pp: case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ Integrable (fun x ↦ (g x).toReal) μ
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case refine_1
𝕜 : 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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ p) ((1 / 2) ^ e)

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ p) ((1 / 2) ^ e)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case smul_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) → ∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = c • x

pp: case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) →
      ∀ ⦃y : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = y) → ∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = x + y

Tactic:
·

Goal state after:
case smul_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) → ∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = c • x
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) →
      ∀ ⦃y : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = y) → ∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = x + y

Tactic:
·

Goal state after:
case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) →
      ∀ ⦃y : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = y) → ∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = x + y
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ (∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ c, 0 < c ∧ c • x ∈ s

pp: case refine_2
𝕜 : 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
⊢ (∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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
⊢ (∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ c, 0 < c ∧ c • x ∈ s
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ (∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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
⊢ (∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case refine_2
𝕜 : 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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ q) ((1 / 2) ^ e)

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ q) ((1 / 2) ^ e)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case refine_1
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ y ∈ Set.Ioo (-1) 1

pp: case refine_2
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ 0 ∈ Set.Icc (-|x|) |x|

pp: case refine_3
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ x ∈ Set.Icc (-|x|) |x|

Tactic:
·

Goal state after:
case refine_1
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ y ∈ Set.Ioo (-1) 1
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: case inl
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hzero : 0 = c
⊢ ⟨c, hc⟩ • x ∈ C

pp: case inr
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ ⟨c, hc⟩ • x ∈ C

Tactic:
·

Goal state after:
case inl
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hzero : 0 = c
⊢ ⟨c, hc⟩ • x ∈ C
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: case inr
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ ⟨c, hc⟩ • x ∈ C

Tactic:
·

Goal state after:
case inr
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ ⟨c, hc⟩ • x ∈ C