awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
refine : y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
⊢ s.WSameSide x z

Tactic:
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
⊢ y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0

Tactic:
fun h => False.elim ?_

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
refine : ∀ (h : y -ᵥ p₂ = 0), False
⊢ y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0

Tactic:
refine fun h => False.elim ?_

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
h : y -ᵥ p₂ = 0
⊢ y = p₂

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Premises used: vsub_eq_zero_iff_eq
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
h : y = p₂
⊢ False

Tactic:
hy (h.symm ▸ hp₂)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
h : y = p₂
⊢ False

Tactic:
exact hy (h.symm ▸ hp₂)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.WSameSide x y
hyz : s.SSameSide y z
⊢ s.WSameSide x z

Tactic:
hxy.trans hyz.1 hyz.2.1

Premises used: AffineSubspace.WSameSide.trans, And.right, And.left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.WSameSide x y
hyz : s.WOppSide y z
hy : y ∉ s
rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)), s.WOppSide x z
⊢ s.WOppSide x z

Tactic:
rcases hxy with ⟨p₁, hp₁, p₂, hp₂, hxy⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hyz : s.WOppSide y z
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)

Tactic:
rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz

Premises used: AffineSubspace.wOppSide_iff_exists_left, or_iff_right
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hyz : s.WOppSide y z
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
hyz₁ : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
⊢ p₂ ∈ s

Tactic:
rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz

Premises used: AffineSubspace.wOppSide_iff_exists_left, or_iff_right
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hyz : s.WOppSide y z
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
hyz₁ : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
hp₃ : p₂ ∈ s
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz

Premises used: AffineSubspace.wOppSide_iff_exists_left, or_iff_right
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hyz : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
rcases : ∀ (p₃ : P) (hp₃ : p₃ ∈ s) (hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)), s.WOppSide x z
⊢ s.WOppSide x z

Tactic:
rcases hyz with ⟨p₃, hp₃, hyz⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
⊢ s.WOppSide x z

Tactic:
⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩

Premises used: And.intro, Exists.intro, SameRay.trans, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
refine : y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ p₃ -ᵥ z = 0
⊢ s.WOppSide x z

Tactic:
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
⊢ y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ p₃ -ᵥ z = 0

Tactic:
fun h => False.elim ?_

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
refine : ∀ (h : y -ᵥ p₂ = 0), False
⊢ y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ p₃ -ᵥ z = 0

Tactic:
refine fun h => False.elim ?_

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
h : y -ᵥ p₂ = 0
⊢ y = p₂

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Premises used: vsub_eq_zero_iff_eq
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
h : y = p₂
⊢ False

Tactic:
hy (h.symm ▸ hp₂)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
h : y = p₂
⊢ False

Tactic:
exact hy (h.symm ▸ hp₂)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.WSameSide x y
hyz : s.SOppSide y z
⊢ s.WOppSide x z

Tactic:
hxy.trans_wOppSide hyz.1 hyz.2.1

Premises used: AffineSubspace.WSameSide.trans_wOppSide, And.right, And.left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SSameSide x y
hyz : s.WSameSide y z
⊢ s.WSameSide x z

Tactic:
(hyz.symm.trans_sSameSide hxy.symm).symm

Premises used: AffineSubspace.WSameSide.trans_sSameSide, AffineSubspace.WSameSide.symm, AffineSubspace.SSameSide.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SSameSide x y
hyz : s.SSameSide y z
⊢ s.SSameSide x z

Tactic:
⟨hxy.wSameSide.trans_sSameSide hyz, hxy.2.1, hyz.2.2⟩

Premises used: AffineSubspace.SSameSide, AffineSubspace.WSameSide.trans_sSameSide, AffineSubspace.SSameSide.wSameSide, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SSameSide x y
hyz : s.WOppSide y z
⊢ s.WOppSide x z

Tactic:
hxy.wSameSide.trans_wOppSide hyz hxy.2.2

Premises used: AffineSubspace.WSameSide.trans_wOppSide, AffineSubspace.SSameSide.wSameSide, And.right
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SSameSide x y
hyz : s.SOppSide y z
⊢ s.SOppSide x z

Tactic:
⟨hxy.trans_wOppSide hyz.1, hxy.2.1, hyz.2.2⟩

Premises used: AffineSubspace.SSameSide.trans_wOppSide, And.right, And.left, And.intro, AffineSubspace.SOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.WOppSide x y
hyz : s.WSameSide y z
hy : y ∉ s
⊢ s.WOppSide x z

Tactic:
(hyz.symm.trans_wOppSide hxy.symm hy).symm

Premises used: AffineSubspace.WSameSide.trans_wOppSide, AffineSubspace.WOppSide.symm, AffineSubspace.WSameSide.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.WOppSide x y
hyz : s.SSameSide y z
⊢ s.WOppSide x z

Tactic:
hxy.trans_wSameSide hyz.1 hyz.2.1

Premises used: AffineSubspace.WOppSide.trans_wSameSide, And.right, And.left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.WOppSide x y
hyz : s.WOppSide y z
hy : y ∉ s
rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)), s.WSameSide x z
⊢ s.WSameSide x z

Tactic:
rcases hxy with ⟨p₁, hp₁, p₂, hp₂, hxy⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hyz : s.WOppSide y z
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)

Tactic:
rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz

Premises used: AffineSubspace.wOppSide_iff_exists_left, or_iff_right
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hyz : s.WOppSide y z
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
hyz₁ : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
⊢ p₂ ∈ s

Tactic:
rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz

Premises used: AffineSubspace.wOppSide_iff_exists_left, or_iff_right
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hyz : s.WOppSide y z
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
hyz₁ : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
hp₃ : p₂ ∈ s
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz

Premises used: AffineSubspace.wOppSide_iff_exists_left, or_iff_right
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hyz : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
rcases : ∀ (p₃ : P) (hp₃ : p₃ ∈ s) (hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)), s.WSameSide x z
⊢ s.WSameSide x z

Tactic:
rcases hyz with ⟨p₃, hp₃, hyz⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
⊢ SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)

Tactic:
rw [← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev] at hyz

Premises used: neg_vsub_eq_vsub_rev, sameRay_neg_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
⊢ s.WSameSide x z

Tactic:
⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩

Premises used: And.intro, Exists.intro, SameRay.trans, AffineSubspace.WSameSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
refine : p₂ -ᵥ y = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
⊢ s.WSameSide x z

Tactic:
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
⊢ p₂ -ᵥ y = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0

Tactic:
fun h => False.elim ?_

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
refine : ∀ (h : p₂ -ᵥ y = 0), False
⊢ p₂ -ᵥ y = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0

Tactic:
refine fun h => False.elim ?_

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
h : p₂ -ᵥ y = 0
⊢ p₂ = y

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Premises used: vsub_eq_zero_iff_eq
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
h : p₂ = y
⊢ False

Tactic:
hy (h ▸ hp₂)

Premises used: Eq.rec
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
h : p₂ = y
⊢ False

Tactic:
exact hy (h ▸ hp₂)

Premises used: Eq.rec
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.WOppSide x y
hyz : s.SOppSide y z
⊢ s.WSameSide x z

Tactic:
hxy.trans hyz.1 hyz.2.1

Premises used: AffineSubspace.WOppSide.trans, And.right, And.left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SOppSide x y
hyz : s.WSameSide y z
⊢ s.WOppSide x z

Tactic:
(hyz.symm.trans_sOppSide hxy.symm).symm

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.WOppSide.symm, AffineSubspace.WSameSide.symm, AffineSubspace.WSameSide.trans_sOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SOppSide x y
hyz : s.SSameSide y z
⊢ s.SOppSide x z

Tactic:
(hyz.symm.trans_sOppSide hxy.symm).symm

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.SSameSide.symm, AffineSubspace.SSameSide.trans_sOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SOppSide x y
hyz : s.WOppSide y z
⊢ s.WSameSide x z

Tactic:
(hyz.symm.trans_sOppSide hxy.symm).symm

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.WOppSide.symm, AffineSubspace.WOppSide.trans_sOppSide, AffineSubspace.WSameSide.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxy : s.SOppSide x y
hyz : s.SOppSide y z
⊢ s.SSameSide x z

Tactic:
⟨hxy.trans_wOppSide hyz.1, hxy.2.1, hyz.2.2⟩

Premises used: AffineSubspace.SSameSide, And.right, And.left, And.intro, AffineSubspace.SOppSide.trans_wOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y : P
mp : s.WSameSide x y ∧ s.WOppSide x y → x ∈ s ∨ y ∈ s
mpr : x ∈ s ∨ y ∈ s → s.WSameSide x y ∧ s.WOppSide x y
⊢ s.WSameSide x y ∧ s.WOppSide x y ↔ x ∈ s ∨ y ∈ s

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y : P
hs : s.WSameSide x y
ho : s.WOppSide x y
⊢ s.WOppSide y x

Tactic:
rw [wOppSide_comm] at ho

Premises used: AffineSubspace.wOppSide_comm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y : P
hs : s.WSameSide x y
ho : s.WOppSide y x
mp : ∀ (h : ¬(x ∈ s ∨ y ∈ s)), False
⊢ x ∈ s ∨ y ∈ s

Tactic:
by_contra h
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y : P
hs : s.WSameSide x y
ho : s.WOppSide y x
h : ¬(x ∈ s ∨ y ∈ s)
⊢ x ∉ s ∧ y ∉ s

Tactic:
rw [not_or] at h

Premises used: not_or
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x y : P
hs : s.WSameSide x y
ho : s.WOppSide y x
h : x ∉ s ∧ y ∉ s
⊢ False

Tactic:
h.1 (wOppSide_self_iff.1 (hs.trans_wOppSide ho h.2))

Premises used: AffineSubspace.WSameSide.trans_wOppSide, AffineSubspace.wOppSide_self_iff, And.right, And.left, Iff.mp