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 : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
⊢ ¬SSameSide.{u_1, u_2, u_4} (R := R) ⊥ x y

Tactic:
fun h => not_wSameSide_bot x y h.wSameSide

Premises used: AffineSubspace.not_wSameSide_bot, AffineSubspace.SSameSide.wSameSide, Not
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
⊢ ¬WOppSide.{u_1, u_2, u_4} (R := R) ⊥ x y

Tactic:
fun ⟨_, h, _⟩ => h.elim

Premises used: False, False.elim, _private.0.AffineSubspace.not_wOppSide_bot.match_1, Not
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
⊢ ¬SOppSide.{u_1, u_2, u_4} (R := R) ⊥ x y

Tactic:
fun h => not_wOppSide_bot x y h.wOppSide

Premises used: AffineSubspace.SOppSide.wOppSide, AffineSubspace.not_wOppSide_bot, Not
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ s.WSameSide x x ↔ (↑s : Set P).Nonempty

Tactic:
⟨fun h => h.nonempty, fun ⟨p, hp⟩ => ⟨p, hp, p, hp, SameRay.rfl⟩⟩

Premises used: AffineSubspace.WSameSide.nonempty, And.intro, Iff.intro, _private.0.AffineSubspace.wSameSide_self_iff.match_1, Exists.intro, SameRay.rfl, AffineSubspace.WSameSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ s.SSameSide x x ↔ (↑s : Set P).Nonempty ∧ x ∉ s

Tactic:
⟨fun ⟨h, hx, _⟩ => ⟨wSameSide_self_iff.1 h, hx⟩, fun ⟨h, hx⟩ => ⟨wSameSide_self_iff.2 h, hx, hx⟩⟩

Premises used: Iff.mpr, AffineSubspace.SSameSide, _private.0.AffineSubspace.sSameSide_self_iff.match_1, Membership.mem, _private.0.AffineSubspace.sSameSide_self_iff.match_2, AffineSubspace.wSameSide_self_iff, And, Set.Nonempty, SetLike.coe, And.intro, Iff.intro, Iff.mp, Not
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
⊢ s.WSameSide x y

Tactic:
⟨x, hx, x, hx, ?_⟩

Premises used: And.intro, Exists.intro, AffineSubspace.WSameSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
refine : SameRay R (x -ᵥ x) (y -ᵥ x)
⊢ s.WSameSide x y

Tactic:
refine ⟨x, hx, x, hx, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
rw : SameRay R 0 (y -ᵥ x)
⊢ SameRay R (x -ᵥ x) (y -ᵥ x)

Tactic:
rw [vsub_self]

Premises used: vsub_self
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
⊢ SameRay R 0 (y -ᵥ x)

Tactic:
apply SameRay.zero_left

Premises used: SameRay.zero_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hy : y ∈ s
⊢ s.WSameSide x y

Tactic:
(wSameSide_of_left_mem x hy).symm

Premises used: AffineSubspace.WSameSide.symm, AffineSubspace.wSameSide_of_left_mem
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
⊢ s.WOppSide x y

Tactic:
⟨x, hx, x, hx, ?_⟩

Premises used: And.intro, Exists.intro, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
refine : SameRay R (x -ᵥ x) (x -ᵥ y)
⊢ s.WOppSide x y

Tactic:
refine ⟨x, hx, x, hx, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
rw : SameRay R 0 (x -ᵥ y)
⊢ SameRay R (x -ᵥ x) (x -ᵥ y)

Tactic:
rw [vsub_self]

Premises used: vsub_self
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hx : x ∈ s
⊢ SameRay R 0 (x -ᵥ y)

Tactic:
apply SameRay.zero_left

Premises used: SameRay.zero_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
hy : y ∈ s
⊢ s.WOppSide x y

Tactic:
(wOppSide_of_left_mem x hy).symm

Premises used: AffineSubspace.wOppSide_of_left_mem, AffineSubspace.WOppSide.symm
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
mp : s.WSameSide (v +ᵥ x) y → s.WSameSide x y
mpr : s.WSameSide x y → s.WSameSide (v +ᵥ x) y
⊢ s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x y

Tactic:
⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩

Premises used: Submodule.neg_mem, HVAdd.hVAdd, AffineSubspace.vadd_mem_of_mem_direction, And.intro, Exists.intro, AffineSubspace.WSameSide, Neg.neg
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
mp : SameRay R (x -ᵥ (-v +ᵥ p₁)) (y -ᵥ p₂)
⊢ s.WSameSide x y

Tactic:
refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
mp : SameRay R (x -ᵥ p₁ - -v) (y -ᵥ p₂)
mp₁ : SameRay R (x -ᵥ p₁ + v) (y -ᵥ p₂)
mp₂ : SameRay R (v + (x -ᵥ p₁)) (y -ᵥ p₂)
mp₃ mp₄ mp₅ mp₆ : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (y -ᵥ p₂)

Tactic:
rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm, sub_neg_eq_add
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide (v +ᵥ x) y

Tactic:
⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, p₂, hp₂, ?_⟩

Premises used: HVAdd.hVAdd, AffineSubspace.vadd_mem_of_mem_direction, And.intro, Exists.intro, AffineSubspace.WSameSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
mpr : SameRay R ((v +ᵥ x) -ᵥ (v +ᵥ p₁)) (y -ᵥ p₂)
⊢ s.WSameSide (v +ᵥ x) y

Tactic:
refine ⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, p₂, hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h mpr mpr₁ mpr₂ mpr₃ : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R ((v +ᵥ x) -ᵥ (v +ᵥ p₁)) (y -ᵥ p₂)

Tactic:
rwa [vadd_vsub_vadd_cancel_left]

Premises used: vadd_vsub_vadd_cancel_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WSameSide (v +ᵥ y) x ↔ s.WSameSide x y
rw₁ : s.WSameSide y x ↔ s.WSameSide x y
rw₂ rw₃ : s.WSameSide x y ↔ s.WSameSide x y
⊢ s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y

Tactic:
rw [wSameSide_comm, wSameSide_vadd_left_iff hv, wSameSide_comm]

Premises used: AffineSubspace.wSameSide_comm, AffineSubspace.wSameSide_vadd_left_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.SSameSide x y
rw₁ : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
rw₂ : s.WSameSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
rw₃ rw₄ : s.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
⊢ s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y

Tactic:
rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]

Premises used: AffineSubspace.SSameSide, AffineSubspace.wSameSide_vadd_left_iff, AffineSubspace.vadd_mem_iff_mem_of_mem_direction
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.SSameSide (v +ᵥ y) x ↔ s.SSameSide x y
rw₁ : s.SSameSide y x ↔ s.SSameSide x y
rw₂ rw₃ : s.SSameSide x y ↔ s.SSameSide x y
⊢ s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y

Tactic:
rw [sSameSide_comm, sSameSide_vadd_left_iff hv, sSameSide_comm]

Premises used: AffineSubspace.sSameSide_comm, AffineSubspace.sSameSide_vadd_left_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
mp : s.WOppSide (v +ᵥ x) y → s.WOppSide x y
mpr : s.WOppSide x y → s.WOppSide (v +ᵥ x) y
⊢ s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide x y

Tactic:
⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩

Premises used: Submodule.neg_mem, HVAdd.hVAdd, AffineSubspace.vadd_mem_of_mem_direction, And.intro, Exists.intro, Neg.neg, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
mp : SameRay R (x -ᵥ (-v +ᵥ p₁)) (p₂ -ᵥ y)
⊢ s.WOppSide x y

Tactic:
refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
mp : SameRay R (x -ᵥ p₁ - -v) (p₂ -ᵥ y)
mp₁ : SameRay R (x -ᵥ p₁ + v) (p₂ -ᵥ y)
mp₂ : SameRay R (v + (x -ᵥ p₁)) (p₂ -ᵥ y)
mp₃ mp₄ mp₅ mp₆ : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (p₂ -ᵥ y)

Tactic:
rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm, sub_neg_eq_add
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide (v +ᵥ x) y

Tactic:
⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, p₂, hp₂, ?_⟩

Premises used: HVAdd.hVAdd, AffineSubspace.vadd_mem_of_mem_direction, And.intro, Exists.intro, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
mpr : SameRay R ((v +ᵥ x) -ᵥ (v +ᵥ p₁)) (p₂ -ᵥ y)
⊢ s.WOppSide (v +ᵥ x) y

Tactic:
refine ⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, p₂, hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h mpr mpr₁ mpr₂ mpr₃ : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R ((v +ᵥ x) -ᵥ (v +ᵥ p₁)) (p₂ -ᵥ y)

Tactic:
rwa [vadd_vsub_vadd_cancel_left]

Premises used: vadd_vsub_vadd_cancel_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WOppSide (v +ᵥ y) x ↔ s.WOppSide x y
rw₁ : s.WOppSide y x ↔ s.WOppSide x y
rw₂ rw₃ : s.WOppSide x y ↔ s.WOppSide x y
⊢ s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y

Tactic:
rw [wOppSide_comm, wOppSide_vadd_left_iff hv, wOppSide_comm]

Premises used: AffineSubspace.wOppSide_comm, AffineSubspace.wOppSide_vadd_left_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WOppSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.SOppSide x y
rw₁ : s.WOppSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
rw₂ : s.WOppSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
rw₃ rw₄ : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
⊢ s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y

Tactic:
rw [SOppSide, SOppSide, wOppSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]

Premises used: AffineSubspace.vadd_mem_iff_mem_of_mem_direction, AffineSubspace.SOppSide, AffineSubspace.wOppSide_vadd_left_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.SOppSide (v +ᵥ y) x ↔ s.SOppSide x y
rw₁ : s.SOppSide y x ↔ s.SOppSide x y
rw₂ rw₃ : s.SOppSide x y ↔ s.SOppSide x y
⊢ s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y

Tactic:
rw [sOppSide_comm, sOppSide_vadd_left_iff hv, sOppSide_comm]

Premises used: AffineSubspace.sOppSide_comm, AffineSubspace.sOppSide_vadd_left_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
⟨p₂, hp₂, p₁, hp₁, ?_⟩

Premises used: And.intro, Exists.intro, AffineSubspace.WSameSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
refine : SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (x -ᵥ p₁)
⊢ s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
rw : SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (x -ᵥ p₁)

Tactic:
rw [vadd_vsub]

Premises used: vadd_vsub
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : 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:
SameRay.sameRay_nonneg_smul_left _ ht

Premises used: SameRay.sameRay_nonneg_smul_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : 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:
exact SameRay.sameRay_nonneg_smul_left _ ht

Premises used: SameRay.sameRay_nonneg_smul_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ s.WSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)

Tactic:
(wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht).symm

Premises used: AffineSubspace.WSameSide.symm, AffineSubspace.wSameSide_smul_vsub_vadd_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
h : x ∈ s
t : R
ht : 0 ≤ t
⊢ s.WSameSide ((lineMap x y : (a : R) → P) t) y

Tactic:
wSameSide_smul_vsub_vadd_left y h h ht

Premises used: AffineSubspace.wSameSide_smul_vsub_vadd_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
h : x ∈ s
t : R
ht : 0 ≤ t
⊢ s.WSameSide y ((lineMap x y : (a : R) → P) t)

Tactic:
(wSameSide_lineMap_left y h ht).symm

Premises used: AffineSubspace.WSameSide.symm, AffineSubspace.wSameSide_lineMap_left
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
⟨p₂, hp₂, p₁, hp₁, ?_⟩

Premises used: And.intro, Exists.intro, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
refine : SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (p₁ -ᵥ x)
⊢ s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
rw : SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (p₁ -ᵥ x)

Tactic:
rw [vadd_vsub, ← neg_neg t, neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]

Premises used: neg_smul, neg_neg, smul_neg, neg_vsub_eq_vsub_rev, vadd_vsub
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : 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:
SameRay.sameRay_nonneg_smul_left _ (neg_nonneg.2 ht)

Premises used: Iff.mpr, SameRay.sameRay_nonneg_smul_left, neg_nonneg
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : 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:
exact SameRay.sameRay_nonneg_smul_left _ (neg_nonneg.2 ht)

Premises used: Iff.mpr, SameRay.sameRay_nonneg_smul_left, neg_nonneg