mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
x : G
hx : x ∈ C
left✝ : x ≠ 0
hxneg : -x ∈ C
⊢ x + -x ∈ C

Tactic:
]

Goal state after:
R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
x : G
hx : x ∈ C
left✝ : x ≠ 0
hxneg : -x ∈ C
⊢ x + -x ∈ C
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
hx : 0 < x
this : HasStrictDerivAt log x⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
]

Goal state after:
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log x⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
⊢ ¬C.Pointed → ¬C.Flat

Tactic:
]

Goal state after:
R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
⊢ ¬C.Pointed → ¬C.Flat
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
⊢ δ * r + δ * r = ε / 2 * r

Tactic:
by ring

Goal state after:
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
⊢ x - x ∈ C

Tactic:
sub_self x

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.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.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
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : a - b ∉ C
⊢ False

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
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : a - b ∉ C
⊢ False
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
hab : a ≤ b
c : G
⊢ b - a ∈ C

Tactic:
]

Goal state after:
R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
hab : a ≤ b
c : G
⊢ b - a ∈ 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✝ : Module R M
⊢ 0 = 0

Tactic:
]

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
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
⊢ ‖(L₁ - L₂) y‖ ≤ 4 * ‖c‖ * ε * ‖y‖

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
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
⊢ ‖(L₁ - L₂) y‖ ≤ 4 * ‖c‖ * ε * ‖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
C₁ C₂ : ConvexCone R M
c : R
hc : 0 < c
x : M
hx : x ∈ ↑C₁
y : M
hy : y ∈ ↑C₂
⊢ c • x + c • y ∈ ↑C₁ + ↑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✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁✝ C₂✝ : ConvexCone R M
x✝ : M
C₁ C₂ : ConvexCone R M
c : R
hc : 0 < c
x : M
hx : x ∈ ↑C₁
y : M
hy : y ∈ ↑C₂
⊢ c • x + c • y ∈ ↑C₁ + ↑C₂
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
hx : x = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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✝ : Module R M
C₁ C₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : ⊤ ≤ Submodule.span R ↑C₁
⊢ ⊤ ≤ Submodule.span R ↑C₂

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : ⊤ ≤ Submodule.span R ↑C₁
⊢ ⊤ ≤ Submodule.span R ↑C₂
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case e'_9
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : ConvexCone R M
h : C.IsReproducing
⊢ ⊤ ≤ Submodule.span R ↑C

Tactic:
]

Goal state after:
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : ConvexCone R M
h : C.IsReproducing
⊢ ⊤ ≤ Submodule.span R ↑C
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : ConvexCone R M
h : ∀ (x : M), x ∈ ↑C - ↑C
x : M
⊢ x ∈ Submodule.span R ↑C

Tactic:
]

Goal state after:
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : ConvexCone R M
h : ∀ (x : M), x ∈ ↑C - ↑C
x : M
⊢ x ∈ Submodule.span R ↑C
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 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), x ∈ ↑C - ↑C

Tactic:
]

Goal state after:
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), x ∈ ↑C - ↑C
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
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
⊢ ε * r + ε * r = 2 * ε * r

Tactic:
by ring

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
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
⊢ 2 * ε * (2 * ‖c‖ * ‖y‖) = 4 * ‖c‖ * ε * ‖y‖

Tactic:
by ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y ↦ Real.log (f y)) ((f x)⁻¹ * f') s x

Tactic:
]

Goal state after:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y ↦ Real.log (f y)) ((f x)⁻¹ * f') s 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
⊢ r • y - r • z = r • y - r • z

Tactic:
]

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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
⊢ ∀ (i : ℕ), x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ i)

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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
⊢ ∀ (i : ℕ), x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ i)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: f : ℝ → ℝ
x f' : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y ↦ Real.log (f y)) (f' / f x) Set.univ x

Tactic:
]

Goal state after:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y ↦ Real.log (f y)) (f' / f x) Set.univ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y ↦ Real.log (f y)) ((f x)⁻¹ * f') x

Tactic:
]

Goal state after:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y ↦ Real.log (f y)) ((f x)⁻¹ * f') x
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
x : M
hs : Convex 𝕜 s
hx : x ∈ hull 𝕜 s
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy : y ∈ r₂ • s
⊢ r₁ • y ∈ r₁ • 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
x : M
hs : Convex 𝕜 s
hx : x ∈ hull 𝕜 s
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy : y ∈ r₂ • s
⊢ r₁ • y ∈ r₁ • 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
s : Set M
x : M
hs : Convex 𝕜 s
hx : x ∈ hull 𝕜 s
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
⊢ y₁ + y₂ ∈ r₁ • s + 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
x : M
hs : Convex 𝕜 s
hx : x ∈ hull 𝕜 s
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
⊢ y₁ + y₂ ∈ r₁ • s + 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 e_a.e_f
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)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
i : ℕ
⊢ y ^ i = y ^ i

Tactic:
]

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
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ Disjoint (↑C) s ↔ Disjoint (↑C) s

Tactic:
]

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
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
⊢ y ∈ 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
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
⊢ y ∈ 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
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ x = x

Tactic:
]

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
x : M
hx : x ∈ s
⊢ x ∈ 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
hx : x ∈ s
⊢ x ∈ s
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
s : Set (Submodule R E)
⊢ ⨅ b ∈ s, ↑b = ⨅ S ∈ s, ↑S

Tactic:
]

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
s : Set (Submodule R E)
⊢ ⨆ b ∈ s, ↑b = ⨆ S ∈ s, ↑S

Tactic:
]

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : E
s : Set E
⊢ (∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x) ↔
    ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r ↦ r • m) = x

Tactic:
]

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : E
s : Set E
⊢ (∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x) ↔
    ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r ↦ r • m) = x
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
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 ∂μ
⊢ (∫⁻ (a : α), ↑(f a) ∂μ).toReal + ↑δ = (∫⁻ (a : α), ↑(f a) ∂μ).toReal + ↑δ

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
x : ↥f.domain
hx : -↑(-x) - y ∈ s
⊢ {x | -↑x - y ∈ s}.Nonempty

Tactic:
]

Goal state after:
case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
x : ↥f.domain
hx : -↑(-x) - y ∈ s
⊢ {x | -↑x - y ∈ s}.Nonempty
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

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

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑(xp - xn) ∈ s
⊢ ↑f xn ≤ ↑f xp

Tactic:
]

Goal state after:
case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑(xp - xn) ∈ s
⊢ ↑f xn ≤ ↑f xp
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑f xn ≤ ↑f xp
⊢ ↑f xn ≤ ↑f xp

Tactic:
]

Goal state after:
case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑f xn ≤ ↑f xp
⊢ ↑f xn ≤ ↑f xp
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
H : f.domain ≤ f.domain ∧ y ∈ ↑f.domain
⊢ False

Tactic:
]

Goal state after:
case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
H : f.domain ≤ f.domain ∧ y ∈ ↑f.domain
⊢ False
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩

Tactic:
]

Goal state after:
case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
⊢ x < 1

Tactic:
]

Goal state after:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
⊢ x < 1
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
x : α
⊢ s.indicator (fun x ↦ c) x ≤ s.indicator (fun x ↦ c) x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
h₁ :
  1 / 2 * log ((1 + x) / (1 - x)) ≤ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) + x ^ (2 * n + 1) / (1 - x ^ 2)
⊢ 1 / 2 * log ((1 + x) / (1 - x)) ≤ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) + x ^ (2 * n + 1) / (1 - x ^ 2)

Tactic:
]

Goal state after:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
h₁ :
  1 / 2 * log ((1 + x) / (1 - x)) ≤ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) + x ^ (2 * n + 1) / (1 - x ^ 2)
⊢ 1 / 2 * log ((1 + x) / (1 - x)) ≤ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) + x ^ (2 * n + 1) / (1 - x ^ 2)