awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
⊢ s.WSameSide x z
have hyz₁ : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
Tactic: rw [← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev] at 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₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
⊢ s.WSameSide x z
have refine : p₂ -ᵥ y = 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₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
⊢ p₂ -ᵥ y = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
have refine : ∀ (h : p₂ -ᵥ y = 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₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
h : p₂ -ᵥ y = 0
⊢ False
have h₁ : p₂ = y
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 : P
⊢ s.WSameSide x y ∧ s.WOppSide x y ↔ x ∈ s ∨ y ∈ s
have mp : s.WSameSide x y ∧ s.WOppSide x y → x ∈ s ∨ y ∈ 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 y : P
mp : s.WSameSide x y ∧ s.WOppSide x y → x ∈ s ∨ y ∈ s
⊢ s.WSameSide x y ∧ s.WOppSide x y ↔ x ∈ s ∨ y ∈ s
have mpr : x ∈ s ∨ y ∈ s → s.WSameSide x 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
hs : s.WSameSide x y
ho : s.WOppSide x y
⊢ x ∈ s ∨ y ∈ s
have ho₁ : s.WOppSide y x
Tactic: rw [wOppSide_comm] at ho
Cleared hypotheses: ho
-- 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
hs : s.WSameSide x y
ho : s.WOppSide y x
⊢ x ∈ s ∨ y ∈ s
have mp : ∀ (h : ¬(x ∈ s ∨ y ∈ s)), False
Tactic: by_contra h
-- 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
hs : s.WSameSide x y
ho : s.WOppSide y x
h : ¬(x ∈ s ∨ y ∈ s)
⊢ False
have h₁ : x ∉ s ∧ y ∉ s
Tactic: rw [not_or] at h
Cleared hypotheses: h
-- 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
h : s.WSameSide x y
ho : s.SOppSide x y
⊢ False
have hxy : x ∈ s ∨ y ∈ s
Tactic: have hxy := wSameSide_and_wOppSide_iff.1 ⟨h, ho.1⟩
-- 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
h : s.WSameSide x y
ho : s.SOppSide x y
hxy : x ∈ s ∨ y ∈ s
⊢ False
have inl : ∀ (hx : x ∈ s), False
Tactic: rcases hxy with (hx | hy)
Cleared hypotheses: 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 : P
h : s.WSameSide x y
ho : s.SOppSide x y
hxy : x ∈ s ∨ y ∈ s
inl : ∀ (hx : x ∈ s), False
⊢ False
have inr : ∀ (hy : y ∈ s), False
Tactic: rcases hxy with (hx | hy)
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 : P
h : s.SSameSide x y
ho : s.WOppSide x y
⊢ False
have hxy : x ∈ s ∨ y ∈ s
Tactic: have hxy := wSameSide_and_wOppSide_iff.1 ⟨h.1, ho⟩
-- 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
h : s.SSameSide x y
ho : s.WOppSide x y
hxy : x ∈ s ∨ y ∈ s
⊢ False
have inl : ∀ (hx : x ∈ s), False
Tactic: rcases hxy with (hx | hy)
Cleared hypotheses: 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 : P
h : s.SSameSide x y
ho : s.WOppSide x y
hxy : x ∈ s ∨ y ∈ s
inl : ∀ (hx : x ∈ s), False
⊢ False
have inr : ∀ (hy : y ∈ s), False
Tactic: rcases hxy with (hx | hy)
Cleared hypotheses: 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 : P
⊢ s.WOppSide x y ↔ ∃ p ∈ s, Wbtw R x p y
have refine : ∀ (h : s.WOppSide x y), ∃ p ∈ s, Wbtw R x p y
Tactic: refine ⟨fun h => ?_, fun ⟨p, hp, h⟩ => h.wOppSide₁₃ 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
h : s.WOppSide x y
⊢ ∃ p ∈ s, Wbtw R x p y
have inl : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (h : x -ᵥ p₁ = 0), ∃ p ∈ s, Wbtw R x p y
Tactic: rcases h with ⟨p₁, hp₁, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, 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 : P
h : s.WOppSide x y
inl : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (h : x -ᵥ p₁ = 0), ∃ p ∈ s, Wbtw R x p y
⊢ ∃ p ∈ s, Wbtw R x p y
have inr : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (h : p₂ -ᵥ y = 0), ∃ p ∈ s, Wbtw R x p y
Tactic: rcases h with ⟨p₁, hp₁, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, 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 : P
h : s.WOppSide x y
inl : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (h : x -ᵥ p₁ = 0), ∃ p ∈ s, Wbtw R x p y
inr : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (h : p₂ -ᵥ y = 0), ∃ p ∈ s, Wbtw R x p y
⊢ ∃ p ∈ s, Wbtw R x p y
have inr₁ : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂)
  (h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)), ∃ p ∈ s, Wbtw R x p y
Tactic: rcases h with ⟨p₁, hp₁, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩
Cleared hypotheses: h
-- 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p₁ = 0
⊢ ∃ p ∈ s, Wbtw R x p y
have h₁ : x = 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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p₁
⊢ ∃ p ∈ s, Wbtw R x p y
have inl : ∃ p ∈ s, Wbtw R p₁ p y
Tactic: rw [h]
-- 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ p ∈ s, Wbtw R x p y
have h₁ : p₂ = y
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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ p ∈ s, Wbtw R x p y
have inr : ∃ p ∈ s, Wbtw R x p p₂
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ ∃ p ∈ s, Wbtw R x p y
have inr : Membership.mem (α := P) s ((lineMap x y : (a : R) → P) (r₂ / (r₁ + r₂)) : P)
Tactic: refine ⟨lineMap x y (r₂ / (r₁ + r₂)), ?_, ?_⟩
-- 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
inr : Membership.mem (α := P) s ((lineMap x y : (a : R) → P) (r₂ / (r₁ + r₂)) : P)
⊢ ∃ p ∈ s, Wbtw R x p y
have inr₁ : Wbtw R x ((lineMap x y : (a : R) → P) (r₂ / (r₁ + r₂))) y
Tactic: refine ⟨lineMap x y (r₂ / (r₁ + r₂)), ?_, ?_⟩
-- 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
have rw : (r₂ / (r₁ + r₂)) • (-(p₂ -ᵥ y) + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
Tactic: rw [← neg_vsub_eq_vsub_rev p₂ y]
-- 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ (r₂ / (r₁ + r₂)) • (-(p₂ -ᵥ y) + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₂ • (p₂ -ᵥ y) -
      ((r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₁ • (x -ᵥ p₁)) =
    0
have match_scalars : r₂ / (r₁ + 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
match_scalars : r₂ / (r₁ + r₂) * -1 + (r₁ + r₂)⁻¹ * (r₂ * 1) = 0
⊢ (r₂ / (r₁ + r₂)) • (-(p₂ -ᵥ y) + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₂ • (p₂ -ᵥ y) -
      ((r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₁ • (x -ᵥ p₁)) =
    0
have match_scalars₁ : r₂ / (r₁ + 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
match_scalars : r₂ / (r₁ + r₂) * -1 + (r₁ + r₂)⁻¹ * (r₂ * 1) = 0
match_scalars₁ : r₂ / (r₁ + r₂) * 1 - r₂ / (r₁ + r₂) * 1 = 0
⊢ (r₂ / (r₁ + r₂)) • (-(p₂ -ᵥ y) + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₂ • (p₂ -ᵥ y) -
      ((r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₁ • (x -ᵥ p₁)) =
    0
have match_scalars₂ : r₂ / (r₁ + r₂) * -1 + 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ (r₂ / (r₁ + r₂)) • (-(p₂ -ᵥ y) + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
have a : (r₂ / (r₁ + r₂)) • (-(p₂ -ᵥ y) + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₂ • (p₂ -ᵥ y) -
    ((r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) + (r₁ + r₂)⁻¹ • r₁ • (x -ᵥ p₁)) =
  0
Tactic: linear_combination (norm := match_scalars <;> field) (r₁ + r₂)⁻¹ • h
-- 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ Membership.mem (α := P) s ((lineMap x y : (a : R) → P) (r₂ / (r₁ + r₂)) : P)
have this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
Tactic: have : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) =
          (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) := by
        rw [← neg_vsub_eq_vsub_rev p₂ y]
        linear_combination (norm := match_scalars <;> field) (r₁ + r₂)⁻¹ • 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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
⊢ Membership.mem (α := P) s ((lineMap x y : (a : R) → P) (r₂ / (r₁ + r₂)) : P)
have inr : (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
Tactic: rw [lineMap_apply, ← vsub_vadd x p₁, ← vsub_vadd y p₂, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc,
        ← vadd_assoc, vadd_eq_add, this]
-- 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
h : s.SOppSide x y
⊢ ∃ p ∈ s, Sbtw R x p y
have obtain : ∀ (p : P) (hp : p ∈ s) (hw : Wbtw R x p y), ∃ p ∈ s, Sbtw R x p y
Tactic: obtain ⟨p, hp, hw⟩ := wOppSide_iff_exists_wbtw.1 h.wOppSide
-- 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
h : s.SOppSide x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
⊢ ∃ p ∈ s, Sbtw R x p y
have refine_1 : p ≠ x
Tactic: refine ⟨p, hp, hw, ?_, ?_⟩
-- 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
h : s.SOppSide x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
refine_1 : p ≠ x
⊢ ∃ p ∈ s, Sbtw R x p y
have refine_2 : p ≠ y
Tactic: refine ⟨p, hp, hw, ?_, ?_⟩
-- 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
h : Sbtw R x y z
hx : x ∉ s
hy : y ∈ s
⊢ s.SOppSide x z
have refine : ∀ (hz : z ∈ s), x ∈ s
Tactic: refine ⟨h.wbtw.wOppSide₁₃ hy, hx, fun hz => 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 z : P
h : Sbtw R x y z
hx : x ∉ s
hy : y ∈ s
hz : z ∈ s
⊢ x ∈ s
have rcases : ∀ (t : R) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P))
  (hyx : (lineMap x z : (a : R) → P) t ≠ x) (hyz : (lineMap x z : (a : R) → P) t ≠ z), x ∈ s
Tactic: rcases h with ⟨⟨t, ⟨ht0, ht1⟩, rfl⟩, hyx, hyz⟩
Cleared hypotheses: y, h, hy
-- 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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
⊢ x ∈ s
have hy₁ : t • (z -ᵥ x) +ᵥ x ∈ s
Tactic: rw [lineMap_apply] at hy
Cleared hypotheses: hy, hyx, hyz
-- 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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
⊢ x ∈ s
have ht : t ≠ 1
Tactic: have ht : t ≠ 1 := by
    rintro rfl
    simp [lineMap_apply] at hyz
-- 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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
ht : t ≠ 1
⊢ x ∈ s
have hy' : (t • (z -ᵥ x) +ᵥ x) -ᵥ z ∈ s.direction
Tactic: have hy' := vsub_mem_direction hy hz
-- 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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
ht : t ≠ 1
hy' : (t • (z -ᵥ x) +ᵥ x) -ᵥ z ∈ s.direction
⊢ x ∈ s
have hy'₁ : z -ᵥ x ∈ s.direction
Tactic: rw [vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev z, ← neg_one_smul R (z -ᵥ x), ← add_smul,
    ← sub_eq_add_neg, s.direction.smul_mem_iff (sub_ne_zero_of_ne ht)] at hy'
Cleared hypotheses: 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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
ht : t ≠ 1
hy' : z -ᵥ x ∈ s.direction
⊢ x ∈ s
have rwa : ∀ (hy : x ∈ s) (hyx : (lineMap x z : (a : R) → P) t ≠ x) (hyz : (lineMap x z : (a : R) → P) t ≠ z) (ht : t ≠ 1)
  (hy' : z -ᵥ x ∈ s.direction), x ∈ s
Tactic: rwa [vadd_mem_iff_mem_of_mem_direction (Submodule.smul_mem _ _ hy')] at hy
Cleared hypotheses: hy, hyx, hyz, ht, 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 p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
⊢ s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x
have refine : ∀ (h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s), x ∈ s
Tactic: refine ⟨wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, 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 p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
⊢ x ∈ s
have rwa : ∀ (h : t • (x -ᵥ p₁) ∈ s.direction), x ∈ s
Tactic: rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne.symm,
    vsub_right_mem_direction_iff_mem hp₁] 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₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
rwa : ∀ (h : t • (x -ᵥ p₁) ∈ s.direction), x ∈ s
⊢ x ∈ s
have rwa₁ : ∀ (h : x -ᵥ p₁ ∈ s.direction), x ∈ s
Tactic: rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne.symm,
    vsub_right_mem_direction_iff_mem hp₁] at h
Cleared hypotheses: h