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
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ s.WOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)

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

Premises used: AffineSubspace.wOppSide_smul_vsub_vadd_left, 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
h : x ∈ s
t : R
ht : t ≤ 0
⊢ s.WOppSide ((lineMap x y : (a : R) → P) t) y

Tactic:
wOppSide_smul_vsub_vadd_left y h h ht

Premises used: AffineSubspace.wOppSide_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 : t ≤ 0
⊢ s.WOppSide y ((lineMap x y : (a : R) → P) t)

Tactic:
(wOppSide_lineMap_left y h ht).symm

Premises used: AffineSubspace.WOppSide.symm, AffineSubspace.wOppSide_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
x y z : P
h : Wbtw R x y z
hx : x ∈ s
rcases : ∀ (t : R) (ht0 : 0 ≤ t), s.WSameSide ((lineMap x z : (a : R) → P) t) z
⊢ s.WSameSide y z

Tactic:
rcases h with ⟨t, ⟨ht0, -⟩, rfl⟩

Premises used: rfl
-- 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 z : P
hx : x ∈ s
t : R
ht0 : 0 ≤ t
⊢ s.WSameSide ((lineMap x z : (a : R) → P) t) z

Tactic:
wSameSide_lineMap_left z hx ht0

Premises used: 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
x z : P
hx : x ∈ s
t : R
ht0 : 0 ≤ t
⊢ s.WSameSide ((lineMap x z : (a : R) → P) t) z

Tactic:
exact wSameSide_lineMap_left z hx ht0

Premises used: 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
x y z : P
h : Wbtw R x y z
hx : x ∈ s
⊢ s.WSameSide z y

Tactic:
(h.wSameSide₂₃ hx).symm

Premises used: Wbtw.wSameSide₂₃, AffineSubspace.WSameSide.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 z : P
h : Wbtw R x y z
hz : z ∈ s
⊢ s.WSameSide x y

Tactic:
h.symm.wSameSide₃₂ hz

Premises used: Wbtw.wSameSide₃₂, Wbtw.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 z : P
h : Wbtw R x y z
hz : z ∈ s
⊢ s.WSameSide y x

Tactic:
h.symm.wSameSide₂₃ hz

Premises used: Wbtw.wSameSide₂₃, Wbtw.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 z : P
h : Wbtw R x y z
hy : y ∈ s
rcases :
  ∀ (t : R) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)),
    s.WOppSide x z
⊢ s.WOppSide x z

Tactic:
rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩

Premises used: rfl
-- 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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
⊢ s.WOppSide x z

Tactic:
⟨_, hy, _, hy, ?_⟩

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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
refine : SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
⊢ s.WOppSide x z

Tactic:
refine ⟨_, hy, _, hy, ?_⟩
-- 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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
inl : ∀ (ht1' : t < 1), SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
inr :
  ∀ (ht0 : LE.le.{u_1} (α := R) 0 1) (ht1 : LE.le.{u_1} (α := R) 1 1)
    (hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) 1 : P)),
    SameRay R (x -ᵥ (lineMap x z : (a : R) → P) 1) ((lineMap x z : (a : R) → P) 1 -ᵥ z)
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)

Tactic:
rcases ht1.lt_or_eq with (ht1' | rfl)

Premises used: LE.le.lt_or_eq, rfl
-- 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 z : P
ht0 : LE.le.{u_1} (α := R) 0 1
ht1 : LE.le.{u_1} (α := R) 1 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) 1 : P)
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) 1) ((lineMap x z : (a : R) → P) 1 -ᵥ z)

Tactic:
simp
-- 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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
ht1' : t < 1
inl : ∀ (ht0' : 0 < t), SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
inl₁ :
  ∀ (ht0 : LE.le.{u_1} (α := R) 0 0) (ht1 : LE.le.{u_1} (α := R) 0 1)
    (hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) 0 : P)) (ht1' : LT.lt.{u_1} (α := R) 0 1),
    SameRay R (x -ᵥ (lineMap x z : (a : R) → P) 0) ((lineMap x z : (a : R) → P) 0 -ᵥ z)
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)

Tactic:
rcases ht0.lt_or_eq with (ht0' | rfl)

Premises used: LE.le.lt_or_eq, rfl
-- 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 z : P
ht0 : LE.le.{u_1} (α := R) 0 0
ht1 : LE.le.{u_1} (α := R) 0 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) 0 : P)
ht1' : LT.lt.{u_1} (α := R) 0 1
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) 0) ((lineMap x z : (a : R) → P) 0 -ᵥ z)

Tactic:
simp
-- 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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)

Tactic:
Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩)

Premises used: Iff.mpr, sub_pos, HSub.hSub, And.intro, Exists.intro, SameRay, OfNat.ofNat, Or.inr
-- 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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
ht1' : t < 1
ht0' : 0 < t
inl : (1 - t) • (x -ᵥ (lineMap x z : (a : R) → P) t) = t • ((lineMap x z : (a : R) → P) t -ᵥ z)
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)

Tactic:
refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩)

Premises used: Or.inr
-- 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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
ht1' : t < 1
ht0' : 0 < t
inl : (1 - t) • (0 - t • (z -ᵥ x)) = t • (t • (z -ᵥ x) + -(z -ᵥ x))
⊢ (1 - t) • (x -ᵥ (lineMap x z : (a : R) → P) t) = t • ((lineMap x z : (a : R) → P) t -ᵥ z)

Tactic:
rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z, vsub_self]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, AffineMap.lineMap_apply, neg_vsub_eq_vsub_rev, 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 z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
ht1' : t < 1
ht0' : 0 < t
⊢ (1 - t) • (0 - t • (z -ᵥ x)) = t • (t • (z -ᵥ x) + -(z -ᵥ x))

Tactic:
module
-- 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 z : P
h : Wbtw R x y z
hy : y ∈ s
⊢ s.WOppSide z x

Tactic:
h.symm.wOppSide₁₃ hy

Premises used: Wbtw.wOppSide₁₃, Wbtw.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 : P
mp : s.WOppSide x x → x ∈ s
mpr : x ∈ s → s.WOppSide x x
⊢ s.WOppSide x x ↔ x ∈ 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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
mp : ∀ (a : R) (h₁ : x -ᵥ p₁ = a • (x -ᵥ p₁ + (p₂ -ᵥ x))), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨a, -, -, -, -, h₁, -⟩ := h.exists_eq_smul_add

Premises used: SameRay.exists_eq_smul_add
-- 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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x -ᵥ p₁ = a • (x -ᵥ p₁ + (p₂ -ᵥ x))
⊢ x = a • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
rw [add_comm, vsub_add_vsub_cancel, ← eq_vadd_iff_vsub_eq] at h₁

Premises used: vsub_add_vsub_cancel, add_comm, eq_vadd_iff_vsub_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 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₁
mp : a • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
⊢ x ∈ s

Tactic:
rw [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 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:
s.smul_vsub_vadd_mem a hp₂ hp₁ hp₁

Premises used: Set.Mem, AffineSubspace.smul_vsub_vadd_mem
-- 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 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:
exact s.smul_vsub_vadd_mem a hp₂ hp₁ hp₁

Premises used: AffineSubspace.smul_vsub_vadd_mem
-- 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 : P
⊢ x ∈ s → s.WOppSide x x

Tactic:
fun h => ⟨x, h, x, h, SameRay.rfl⟩

Premises used: And.intro, Exists.intro, SameRay.rfl, 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 : P
⊢ x ∈ s → s.WOppSide x x

Tactic:
exact fun h => ⟨x, h, x, h, SameRay.rfl⟩
-- 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 : P
⊢ ¬(s.WOppSide x x ∧ x ∉ s ∧ x ∉ s)

Tactic:
simp
-- 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₁ : P
h : p₁ ∈ s
mp : s.WSameSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
mpr : (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) → s.WSameSide x y
⊢ s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

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₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x = p₁'

Tactic:
rw [vsub_eq_zero_iff_eq] at h0

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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
mp : p₁' ∈ s ∨ ∃ p₂ ∈ s, SameRay R (p₁' -ᵥ p₁) (y -ᵥ p₂)
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [h0]
-- 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₁ : 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:
Or.inl hp₁'

Premises used: Or.inl
-- 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₁ : 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:
exact Or.inl hp₁'

Premises used: Or.inl
-- 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₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
Or.inr ⟨p₂', hp₂', ?_⟩

Premises used: And.intro, Exists.intro, Or.inr
-- 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₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
mp : SameRay R (x -ᵥ p₁) (y -ᵥ p₂')
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
refine Or.inr ⟨p₂', hp₂', ?_⟩

Premises used: Or.inr
-- 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₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
mp : SameRay R (x -ᵥ p₁) 0
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂')

Tactic:
rw [h0]
-- 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₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) 0

Tactic:
SameRay.zero_right _

Premises used: SameRay.zero_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 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:
exact SameRay.zero_right _

Premises used: SameRay.zero_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 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₂')
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
Or.inr ⟨(r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂',
        Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩

Premises used: AffineSubspace.smul_vsub_vadd_mem, HDiv.hDiv, VSub.vsub, HVAdd.hVAdd, And.intro, Exists.intro, HSMul.hSMul, Or.inr
-- 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₁ : 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₂')
mp : r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
refine Or.inr ⟨(r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂',
        Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩

Premises used: Or.inr
-- 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₁ : 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₂')
mp : r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ p₂' - (r₁ / r₂) • (p₁ -ᵥ p₁'))
mp₁ : r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ p₂') - r₂ • (r₁ / r₂) • (p₁ -ᵥ p₁')
mp₂ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - r₂ • (r₁ / r₂) • (p₁ -ᵥ p₁')
mp₃ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - (r₂ * (r₁ / r₂)) • (p₁ -ᵥ p₁')
mp₄ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - r₁ • (p₁ -ᵥ p₁')
mp₅ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁'))
mp₆ mp₇ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁)
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))

Tactic:
rw [vsub_vadd_eq_vsub_sub, smul_sub, ← hr, smul_smul, mul_div_cancel₀ _ hr₂.ne.symm,
        ← smul_sub, vsub_sub_vsub_cancel_right]

Premises used: vsub_vadd_eq_vsub_sub, smul_smul, Ne.symm, mul_div_cancel₀, smul_sub, vsub_sub_vsub_cancel_right, LT.lt.ne
-- 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₁ : P
h : p₁ ∈ s
h' : x ∈ s
⊢ s.WSameSide x y

Tactic:
wSameSide_of_left_mem y h'

Premises used: AffineSubspace.wSameSide_of_left_mem
-- 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₁ : P
h : p₁ ∈ s
h' : x ∈ s
⊢ s.WSameSide x y

Tactic:
exact wSameSide_of_left_mem y h'

Premises used: AffineSubspace.wSameSide_of_left_mem
-- 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₁ : P
h : p₁ ∈ s
h₁ : P
h₂ : h₁ ∈ s
h₃ : SameRay R (x -ᵥ p₁) (y -ᵥ h₁)
⊢ s.WSameSide x y

Tactic:
⟨p₁, h, h₁, h₂, h₃⟩

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 : 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₁ : P
h : p₁ ∈ s
h₁ : P
h₂ : h₁ ∈ s
h₃ : SameRay R (x -ᵥ p₁) (y -ᵥ h₁)
⊢ s.WSameSide x y

Tactic:
exact ⟨p₁, h, h₁, h₂, 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₂ : P
h : p₂ ∈ s
rw : (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [wSameSide_comm, wSameSide_iff_exists_left h]

Premises used: AffineSubspace.wSameSide_comm, AffineSubspace.wSameSide_iff_exists_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 p₂ : P
h : p₂ ∈ s
⊢ (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
simp_rw [SameRay.sameRay_comm]

Premises used: SameRay.sameRay_comm