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 : 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
⊢ s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y
have rw₁ : s.WOppSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SOppSide, SOppSide, wOppSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y
have rw₂ : s.WOppSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SOppSide, SOppSide, wOppSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y
have rw₃ : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SOppSide, SOppSide, wOppSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y
have rw : s.SOppSide (v +ᵥ y) x ↔ s.SOppSide x y
Tactic: rw [sOppSide_comm, sOppSide_vadd_left_iff hv, sOppSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y
have rw₁ : s.SOppSide y x ↔ s.SOppSide x y
Tactic: rw [sOppSide_comm, sOppSide_vadd_left_iff hv, sOppSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y
have rw₂ : s.SOppSide x y ↔ s.SOppSide x y
Tactic: rw [sOppSide_comm, sOppSide_vadd_left_iff hv, sOppSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (x -ᵥ p₁)
Tactic: refine ⟨p₂, hp₂, 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 : 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₁) +ᵥ p₂) -ᵥ p₂) (x -ᵥ p₁)
have rw : SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)
Tactic: rw [vadd_vsub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (p₁ -ᵥ x)
Tactic: refine ⟨p₂, hp₂, 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 : 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 • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (p₁ -ᵥ x)
have rw : SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)
Tactic: rw [vadd_vsub, ← neg_neg t, neg_smul, ← smul_neg, 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 : 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 y z
have rcases : ∀ (t : R) (ht0 : 0 ≤ t), s.WSameSide ((lineMap x z : (a : R) → P) t) z
Tactic: rcases h with ⟨t, ⟨ht0, -⟩, rfl⟩
Cleared hypotheses: y, 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 : 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 x z
have 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
Tactic: rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩
Cleared hypotheses: y, h, 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 : 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
have refine : SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
Tactic: refine ⟨_, hy, _, 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 : 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)
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
have inl : ∀ (ht1' : t < 1), 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)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
have 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)
Tactic: rcases ht1.lt_or_eq with (ht1' | rfl)
Cleared hypotheses: t, ht0, ht1, 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 : 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
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
have inl : ∀ (ht0' : 0 < t), 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)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ SameRay R (x -ᵥ (lineMap x z : (a : R) → P) t) ((lineMap x z : (a : R) → P) t -ᵥ z)
have 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)
Tactic: rcases ht0.lt_or_eq with (ht0' | rfl)
Cleared hypotheses: t, ht0, ht1, hy, ht1'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
have inl : (1 - t) • (x -ᵥ (lineMap x z : (a : R) → P) t) = t • ((lineMap x z : (a : R) → P) t -ᵥ z)
Tactic: refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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) • (x -ᵥ (lineMap x z : (a : R) → P) t) = t • ((lineMap x z : (a : R) → P) t -ᵥ z)
have inl : (1 - t) • (0 - t • (z -ᵥ x)) = t • (t • (z -ᵥ x) + -(z -ᵥ x))
Tactic: rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z, vsub_self]
-- 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 : P
⊢ s.WOppSide x x ↔ x ∈ s
have mp : s.WOppSide x x → x ∈ s
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 : P
mp : s.WOppSide x x → x ∈ s
⊢ s.WOppSide x x ↔ x ∈ s
have mpr : x ∈ s → s.WOppSide x 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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
⊢ x ∈ s
have mp : ∀ (a : R) (h₁ : x -ᵥ p₁ = a • (x -ᵥ p₁ + (p₂ -ᵥ x))), x ∈ s
Tactic: obtain ⟨a, -, -, -, -, h₁, -⟩ := h.exists_eq_smul_add
-- 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 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 ∈ s
have h₂ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: rw [add_comm, vsub_add_vsub_cancel, ← eq_vadd_iff_vsub_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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ x ∈ s
have mp : a • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
Tactic: rw [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
⊢ s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have mp : s.WSameSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
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.WSameSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have mpr : (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) → s.WSameSide 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₁) (y -ᵥ p₂)
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₁) (y -ᵥ p₂)
have mp : p₁' ∈ s ∨ ∃ p₂ ∈ s, SameRay R (p₁' -ᵥ p₁) (y -ᵥ p₂)
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 : y -ᵥ p₂' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have mp : SameRay R (x -ᵥ p₁) (y -ᵥ p₂')
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 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂')
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₂ • (y -ᵥ p₂')
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have mp : r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ 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₂, ?_⟩)⟩
-- 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₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
have mp : r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ p₂' - (r₁ / r₂) • (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]
-- 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₂ • (y -ᵥ p₂')
mp : r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ p₂' - (r₁ / r₂) • (p₁ -ᵥ p₁'))
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
have mp₁ : r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ p₂') - r₂ • (r₁ / r₂) • (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]
-- 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₂ • (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₁')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
have mp₂ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - r₂ • (r₁ / r₂) • (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]
-- 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₂ • (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₁')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
have mp₃ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - (r₂ * (r₁ / r₂)) • (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]
-- 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₂ • (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₁')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
have mp₄ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - r₁ • (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]
-- 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₂ • (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₁')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
have mp₅ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ 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]
-- 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₂ • (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₁'))
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
have mp₆ : r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ 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]
-- 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.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have rw : (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Tactic: rw [wSameSide_comm, wSameSide_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
⊢ s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
have rw : x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
Tactic: rw [SSameSide, and_comm, wSameSide_iff_exists_left h, and_assoc, and_congr_right_iff]