mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)

Tactic:
]

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: a b : ℝ
hab : a ≤ b
⊢ sphere ((a + b) / 2) ((b - a) / 2) = {a, b}

Tactic:
]

Goal state after:
a b : ℝ
hab : a ≤ b
⊢ sphere ((a + b) / 2) ((b - a) / 2) = {a, b}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
]

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x y ↔ s.WSameSide x y

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v

Tactic:
simp only [mem_incidenceSet, mem_neighborSet]

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = s(v, Sym2.Mem.other h)

Tactic:
]

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = s(v, Sym2.Mem.other h)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide x y ↔ s.SSameSide x y

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∩ Gᶜ.neighborSet v ⊆ ∅

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∩ Gᶜ.neighborSet v ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : v ≠ w ∧ ¬G.Adj v w
⊢ w ∈ ∅

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : v ≠ w ∧ ¬G.Adj v w
⊢ w ∈ ∅
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
]

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
]

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x y ↔ s.WOppSide x y

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
he✝ : e ∈ G.edgeSet
hv : v ∈ e
he : G.Adj v (Sym2.Mem.other' hv)
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
he✝ : e ∈ G.edgeSet
hv : v ∈ e
he : G.Adj v (Sym2.Mem.other' hv)
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SOppSide x y ↔ s.SOppSide x y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ (1 - t) • (0 - t • (z -ᵥ x)) = t • (t • (z -ᵥ x) + -(z -ᵥ x))

Tactic:
]

Goal state after:
case inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ (1 - t) • (0 - t • (z -ᵥ x)) = t • (t • (z -ᵥ x) + -(z -ᵥ x))
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : 0 ≤ c₁ * c₂
⊢ SameRay R (c₁ • m) (c₂ • m)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : 0 ≤ c₁ * c₂
⊢ SameRay R (c₁ • m) (c₂ • m)
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
⊢ -(c₂ • m) = -(c₂ • m)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₁
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
]

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₁
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
h₂' : p₂ -ᵥ y = -c₂ • m
⊢ SameRay R (c₁ • m) (-c₂ • m)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
h₂' : p₂ -ᵥ y = -c₂ • m
⊢ SameRay R (c₁ • m) (-c₂ • m)
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₃
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
]

Goal state after:
case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₃
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
h₂' : p₂ -ᵥ y = -c₂ • m
⊢ 0 ≤ -(c₁ * c₂)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
h₂' : p₂ -ᵥ y = -c₂ • m
⊢ 0 ≤ -(c₁ * c₂)
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : ∃ x ∈ Set.Ioo 0 1, (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
]

Goal state after:
case inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : ∃ x ∈ Set.Ioo 0 1, (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ x ∈ s

Tactic:
]

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ x ∈ s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ a • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s

Tactic:
]

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ a • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
⊢ ∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, z}

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
⊢ ∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, z}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ ¬(s.WOppSide x x ∧ x ∉ s ∧ x ∉ s)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ ¬(s.WOppSide x x ∧ x ∉ s ∧ x ∉ s)
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x_1 ∈ segment 𝕜 u v, x_1 ∈ (convexHull 𝕜) {p, q, 0 • x + bz • y}

Tactic:
]

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x_1 ∈ segment 𝕜 u v, x_1 ∈ (convexHull 𝕜) {p, q, 0 • x + bz • y}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
]

Goal state after:
case mp.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ p₁' ∈ s ∨ ∃ p₂ ∈ s, SameRay R (p₁' -ᵥ p₁) (y -ᵥ p₂)

Tactic:
]

Goal state after:
case mp.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ p₁' ∈ s ∨ ∃ p₂ ∈ s, SameRay R (p₁' -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, y}

Tactic:
]

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, y}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) 0

Tactic:
]

Goal state after:
case mp.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) 0
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : r < dist p₂ p
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
]

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : r < dist p₂ p
⊢ Wbtw ℝ p₁ p₂ p₃
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁)

Tactic:
]

Goal state after: