awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have rw : (y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Tactic: rw [or_iff_right hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have rw : (x ∉ s ∧ y ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Tactic: rw [sSameSide_comm, sSameSide_iff_exists_left h, ← and_assoc, and_comm (a := y ∉ s), and_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mp : s.WOppSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.WOppSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mpr : (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) → s.WOppSide x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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 ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have h0₁ : x = p₁'
Tactic: rw [vsub_eq_zero_iff_eq] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₁'
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mp : p₁' ∈ s ∨ ∃ p₂ ∈ s, SameRay R (p₁' -ᵥ p₁) (p₂ -ᵥ y)
Tactic: rw [h0]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 : p₂' -ᵥ y = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mp : SameRay R (x -ᵥ p₁) (p₂' -ᵥ y)
Tactic: refine Or.inr ⟨p₂', hp₂', ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 : p₂' -ᵥ y = 0
⊢ SameRay R (x -ᵥ p₁) (p₂' -ᵥ y)
have mp : SameRay R (x -ᵥ p₁) 0
Tactic: rw [h0]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂ • (p₂' -ᵥ y)
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mp : r₁ • (x -ᵥ p₁) = r₂ • (((-r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂') -ᵥ y)
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₂, ?_⟩)⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂ • (p₂' -ᵥ y)
⊢ r₁ • (x -ᵥ p₁) = r₂ • (((-r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂') -ᵥ y)
have mp : r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁')) = r₂ • ((-r₁ / r₂) • (p₁ -ᵥ p₁') + (p₂' -ᵥ y))
Tactic: rw [vadd_vsub_assoc, ← vsub_sub_vsub_cancel_right x p₁ p₁']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂ • (p₂' -ᵥ y)
⊢ r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁')) + r₂ • (p₂' -ᵥ y) - (r₂ • ((-r₁ / r₂) • (p₁ -ᵥ p₁') + (p₂' -ᵥ y)) + r₁ • (x -ᵥ p₁')) = 0
have match_scalars : r₁ * 1 - r₁ * 1 = 0
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂ • (p₂' -ᵥ y)
match_scalars : r₁ * 1 - r₁ * 1 = 0
⊢ r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁')) + r₂ • (p₂' -ᵥ y) - (r₂ • ((-r₁ / r₂) • (p₁ -ᵥ p₁') + (p₂' -ᵥ y)) + r₁ • (x -ᵥ p₁')) = 0
have match_scalars₁ : r₁ * -1 - r₂ * (-r₁ / r₂ * 1) = 0
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂ • (p₂' -ᵥ y)
match_scalars : r₁ * 1 - r₁ * 1 = 0
match_scalars₁ : r₁ * -1 - r₂ * (-r₁ / r₂ * 1) = 0
⊢ r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁')) + r₂ • (p₂' -ᵥ y) - (r₂ • ((-r₁ / r₂) • (p₁ -ᵥ p₁') + (p₂' -ᵥ y)) + r₁ • (x -ᵥ p₁')) = 0
have match_scalars₂ : r₂ * 1 - r₂ * 1 = 0
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂ • (p₂' -ᵥ y)
⊢ r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁')) = r₂ • ((-r₁ / r₂) • (p₁ -ᵥ p₁') + (p₂' -ᵥ y))
have a : r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁')) + r₂ • (p₂' -ᵥ y) - (r₂ • ((-r₁ / r₂) • (p₁ -ᵥ p₁') + (p₂' -ᵥ y)) + r₁ • (x -ᵥ p₁')) = 0
Tactic: linear_combination (norm := match_scalars <;> field) hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.WOppSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have rw : (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Tactic: rw [wOppSide_comm, wOppSide_iff_exists_left h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂) (p₂_1 -ᵥ x)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mp : (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)) → y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 : (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)) → y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mpr : (y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) → y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have mp : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
Tactic: refine Or.inr ⟨p, hp, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ SameRay R (x -ᵥ p) (p₂ -ᵥ y)
have mp : SameRay R (p₂ -ᵥ y) (x -ᵥ p)
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
mp : SameRay R (p₂ -ᵥ y) (x -ᵥ p)
⊢ SameRay R (x -ᵥ p) (p₂ -ᵥ y)
have mp₁ : SameRay R (-(p₂ -ᵥ y)) (-(x -ᵥ p))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
mp : SameRay R (p₂ -ᵥ y) (x -ᵥ p)
mp₁ : SameRay R (-(p₂ -ᵥ y)) (-(x -ᵥ p))
⊢ SameRay R (x -ᵥ p) (p₂ -ᵥ y)
have mp₂ : SameRay R (y -ᵥ p₂) (-(x -ᵥ p))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)
have mpr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
Tactic: refine Or.inr ⟨p, hp, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ SameRay R (y -ᵥ p₂) (p -ᵥ x)
have mpr : SameRay R (p -ᵥ x) (y -ᵥ p₂)
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
mpr : SameRay R (p -ᵥ x) (y -ᵥ p₂)
⊢ SameRay R (y -ᵥ p₂) (p -ᵥ x)
have mpr₁ : SameRay R (-(p -ᵥ x)) (-(y -ᵥ p₂))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
mpr : SameRay R (p -ᵥ x) (y -ᵥ p₂)
mpr₁ : SameRay R (-(p -ᵥ x)) (-(y -ᵥ p₂))
⊢ SameRay R (y -ᵥ p₂) (p -ᵥ x)
have mpr₂ : SameRay R (x -ᵥ p) (-(y -ᵥ p₂))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have rw : x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
Tactic: rw [SOppSide, and_comm, wOppSide_iff_exists_left h, and_assoc, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have rw : (y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Tactic: rw [or_iff_right hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have rw : x ∉ s → y ∉ s → ((y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
Tactic: rw [SOppSide, and_comm, wOppSide_iff_exists_right h, and_assoc, and_congr_right_iff,
    and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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_1 : x ∉ s
hy : y ∉ s
⊢ (y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
have rw : (∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Tactic: rw [or_iff_right hy]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.WSameSide y z
hy : y ∉ s
⊢ s.WSameSide x z
have rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)), s.WSameSide x z
Tactic: rcases hxy with ⟨p₁, hp₁, p₂, hp₂, hxy⟩
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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.WSameSide y z
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x z
have hyz₁ : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (z -ᵥ p₂_1)
Tactic: rw [wSameSide_iff_exists_left hp₂, or_iff_right hy] at hyz
Cleared hypotheses: hyz, hp₂, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂) (z -ᵥ p₂_1)
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x z
have rcases : ∀ (p₃ : P) (hp₃ : p₃ ∈ s) (hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)), s.WSameSide x z
Tactic: rcases hyz with ⟨p₃, hp₃, hyz⟩
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₃)
⊢ s.WSameSide x z
have refine : y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
Tactic: refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : ∀ (h : y -ᵥ p₂ = 0), False
Tactic: refine fun h => False.elim ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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
⊢ False
have h₁ : y = p₂
Tactic: rw [vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.WOppSide x z
have rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)), s.WOppSide x z
Tactic: rcases hxy with ⟨p₁, hp₁, p₂, hp₂, hxy⟩
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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₂)
⊢ s.WOppSide x z
have hyz₁ : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
Tactic: rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz
Cleared hypotheses: hyz, hp₂, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
⊢ s.WOppSide x z
have rcases : ∀ (p₃ : P) (hp₃ : p₃ ∈ s) (hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)), s.WOppSide x z
Tactic: rcases hyz with ⟨p₃, hp₃, hyz⟩
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ p₃ -ᵥ z = 0
Tactic: refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : ∀ (h : y -ᵥ p₂ = 0), False
Tactic: refine fun h => False.elim ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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
⊢ False
have h₁ : y = p₂
Tactic: rw [vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.WSameSide x z
have rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)), s.WSameSide x z
Tactic: rcases hxy with ⟨p₁, hp₁, p₂, hp₂, hxy⟩
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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)
⊢ s.WSameSide x z
have hyz₁ : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)
Tactic: rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz
Cleared hypotheses: hyz, hp₂, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ s.WSameSide x z
have rcases : ∀ (p₃ : P) (hp₃ : p₃ ∈ s) (hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)), s.WSameSide x z
Tactic: rcases hyz with ⟨p₃, hp₃, hyz⟩
Cleared hypotheses: hyz