awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₃ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₄ : t₁ • t₂ • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₅ : (t₁ • t₂) • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₆ : (t₁ • t₂) • (z -ᵥ x) + (t₁ • t₂) • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₇ : (t₁ • t₂) • (z -ᵥ x) + (t₁ • t₂) • (x -ᵥ w) = (t₁ • t₂) • (z -ᵥ w)
refine_2₈ : (t₁ • t₂) • (z -ᵥ x + (x -ᵥ w)) = (t₁ • t₂) • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₉ : (t₁ • t₂) • (z -ᵥ w) = (t₁ • t₂) • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ Collinear R (P := P) {x, y, z}
have this : Eq (α := Set P) {y, x, z} {x, y, z}
Tactic: have : {y, x, z} = {x, y, z} := Set.insert_comm y x {z}
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
h : Collinear R (P := P) {x, y, z}
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
have h₁ : ∃ (v : V), ∀ (p : P), Membership.mem (γ := Set P) {x, y, z} p → ∃ (r : R), p = r • v +ᵥ x
Tactic: rw [collinear_iff_of_mem (Set.mem_insert _ _)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
h : ∃ (v : V), ∀ (p : P), Membership.mem (γ := Set P) {x, y, z} p → ∃ (r : R), p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
have rcases : ∀ (v : V) (h : ∀ (p : P), Membership.mem (γ := Set P) {x, y, z} p → ∃ (r : R), p = r • v +ᵥ x),
  Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
Tactic: rcases h with ⟨v, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
v : V
h : ∀ (p : P), Membership.mem (γ := Set P) {x, y, z} p → ∃ (r : R), p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
have h₁ : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ (r : R), p = r • v +ᵥ x
Tactic: simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
v : V
h : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ (r : R), p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
have hy : ∃ (r : R), y = r • v +ᵥ x
Tactic: have hy := h y (Or.inr (Or.inl rfl))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
v : V
h : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ (r : R), p = r • v +ᵥ x
hy : ∃ (r : R), y = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
have hz : ∃ (r : R), z = r • v +ᵥ x
Tactic: have hz := h z (Or.inr (Or.inr rfl))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
v : V
h : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ (r : R), p = r • v +ᵥ x
hy : ∃ (r : R), y = r • v +ᵥ x
hz : ∃ (r : R), z = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
have rcases : ∀ (ty : R) (h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = z → ∃ (r : R), p = r • v +ᵥ x),
  Wbtw R x (ty • v +ᵥ x) z ∨ Wbtw R (ty • v +ᵥ x) z x ∨ Wbtw R z x (ty • v +ᵥ x)
Tactic: rcases hy with ⟨ty, rfl⟩
Cleared hypotheses: y, h, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x z : P
v : V
hz : ∃ (r : R), z = r • v +ᵥ x
ty : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = z → ∃ (r : R), p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) z ∨ Wbtw R (ty • v +ᵥ x) z x ∨ Wbtw R z x (ty • v +ᵥ x)
have rcases : ∀ (tz : R) (h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x),
  Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases hz with ⟨tz, rfl⟩
Cleared hypotheses: z, hz, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inl : ∀ (hy0 : ty < 0),
  Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy ty 0 with (hy0 | rfl | hy0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
inl :
  ∀ (hy0 : ty < 0),
    Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inr : ∀
  (h :
    ∀ (p : P), p = x ∨ p = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x),
  Wbtw R x (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) (tz • v +ᵥ x) ∨
    Wbtw R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) (tz • v +ᵥ x) x ∨
      Wbtw R (tz • v +ᵥ x) x (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x)
Tactic: rcases lt_trichotomy ty 0 with (hy0 | rfl | hy0)
Cleared hypotheses: ty, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
inl :
  ∀ (hy0 : ty < 0),
    Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
inr :
  ∀
    (h :
      ∀ (p : P),
        p = x ∨ p = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x),
    Wbtw R x (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) (tz • v +ᵥ x) ∨
      Wbtw R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) (tz • v +ᵥ x) x ∨
        Wbtw R (tz • v +ᵥ x) x (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x)
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inr₁ : ∀ (hy0 : 0 < ty),
  Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy ty 0 with (hy0 | rfl | hy0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : ty < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inl : ∀ (hz0 : tz < 0),
  Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : ty < 0
inl :
  ∀ (hz0 : tz < 0),
    Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inl₁ : ∀
  (h :
    ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x),
  Wbtw R x (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) ∨
    Wbtw R (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x ∨
      Wbtw R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
Cleared hypotheses: tz, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : ty < 0
inl :
  ∀ (hz0 : tz < 0),
    Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
inl₁ :
  ∀
    (h :
      ∀ (p : P),
        p = x ∨ p = ty • v +ᵥ x ∨ p = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x),
    Wbtw R x (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) ∨
      Wbtw R (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x ∨
        Wbtw R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x (ty • v +ᵥ x)
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inl₂ : ∀ (hz0 : 0 < tz),
  Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inl : Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rw [wbtw_comm (z := x)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inl : (Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x)) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rw [← or_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : 0 < ty
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inr : ∀ (hz0 : tz < 0),
  Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : 0 < ty
inr :
  ∀ (hz0 : tz < 0),
    Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inr₁ : ∀
  (h :
    ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x),
  Wbtw R x (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) ∨
    Wbtw R (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x ∨
      Wbtw R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
Cleared hypotheses: tz, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : 0 < ty
inr :
  ∀ (hz0 : tz < 0),
    Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
inr₁ :
  ∀
    (h :
      ∀ (p : P),
        p = x ∨ p = ty • v +ᵥ x ∨ p = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x),
    Wbtw R x (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) ∨
      Wbtw R (ty • v +ᵥ x) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x ∨
        Wbtw R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v +ᵥ x) x (ty • v +ᵥ x)
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inr₂ : ∀ (hz0 : 0 < tz),
  Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inr : Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rw [wbtw_comm (z := x)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ (r : R), p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
have inr : (Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x)) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Tactic: rw [← or_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
h : SameRay R (y -ᵥ x) (z -ᵥ x)
⊢ Wbtw R x y z ∨ Wbtw R x z y
have inl : ∀ (h : y -ᵥ x = 0), Wbtw R x y z ∨ Wbtw R x z y
Tactic: rcases h with (h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
h : SameRay R (y -ᵥ x) (z -ᵥ x)
inl : ∀ (h : y -ᵥ x = 0), Wbtw R x y z ∨ Wbtw R x z y
⊢ Wbtw R x y z ∨ Wbtw R x z y
have inr : ∀ (h : z -ᵥ x = 0), Wbtw R x y z ∨ Wbtw R x z y
Tactic: rcases h with (h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
h : SameRay R (y -ᵥ x) (z -ᵥ x)
inl : ∀ (h : y -ᵥ x = 0), Wbtw R x y z ∨ Wbtw R x z y
inr : ∀ (h : z -ᵥ x = 0), Wbtw R x y z ∨ Wbtw R x z y
⊢ Wbtw R x y z ∨ Wbtw R x z y
have inr₁ : ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)), Wbtw R x y z ∨ Wbtw R x z y
Tactic: rcases h with (h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
⊢ Wbtw R x y z ∨ Wbtw R x z y
have inr : ∀
  (this :
    ∀ {y z : P} (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)) (hr : r₂ ≤ r₁),
      Wbtw R x y z ∨ Wbtw R x z y)
  (hr : ¬r₂ ≤ r₁), Wbtw R x y z ∨ Wbtw R x z y
Tactic: wlog hr : r₂ ≤ r₁ generalizing r₁ r₂ y z
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
inr :
  ∀
    (this :
      ∀ {y z : P} (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)) (hr : r₂ ≤ r₁),
        Wbtw R x y z ∨ Wbtw R x z y)
    (hr : ¬r₂ ≤ r₁), Wbtw R x y z ∨ Wbtw R x z y
⊢ Wbtw R x y z ∨ Wbtw R x z y
have wlog : ∀ {y z : P} (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)) (hr : r₂ ≤ r₁),
  Wbtw R x y z ∨ Wbtw R x z y
Tactic: wlog hr : r₂ ≤ r₁ generalizing r₁ r₂ y z
Cleared hypotheses: y, z, r₁, r₂, hr₁, hr₂, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
this :
  ∀ {y z : P} (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)) (hr : r₂ ≤ r₁),
    Wbtw R x y z ∨ Wbtw R x z y
hr : ¬r₂ ≤ r₁
⊢ Wbtw R x y z ∨ Wbtw R x z y
have inr : Wbtw R x z y ∨ Wbtw R x y z
Tactic: rw [or_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
⊢ Wbtw R x y z ∨ Wbtw R x z y
have h₁ : Wbtw R x y z
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
⊢ Wbtw R x y z
have h₁ : (lineMap x z : (a : R) → P) (r₂ / r₁) = y
Tactic: refine ⟨r₂ / r₁, ⟨div_nonneg hr₂.le hr₁.le, div_le_one_of_le₀ hr hr₁.le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
⊢ (lineMap x z : (a : R) → P) (r₂ / r₁) = y
have h' : y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x
Tactic: have h' : y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x := by simp [← h, hr₁.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
h' : y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x
⊢ (lineMap x z : (a : R) → P) (r₂ / r₁) = y
have h₁ : (r₂ / r₁) • (z -ᵥ x) = (r₁⁻¹ * r₂) • (z -ᵥ x)
Tactic: simp only [lineMap_apply, h', vadd_vsub_assoc, smul_smul, eq_vadd_iff_vsub_eq, vsub_self,
    add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (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
ι : Type u_6
i j k : ι
h : Function.Injective ![i, j, k]
T : ι → P
hT : AffineIndependent R T
⊢ ¬Wbtw R (T i) (T j) (T k)
have hT₁ : AffineIndependent R (ι := Fin (Nat.succ 0).succ.succ)
  (T ∘ (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } : (a : Fin (Nat.succ 0).succ.succ) → ι))
Tactic: replace hT := hT.comp_embedding ⟨_, h⟩
Cleared hypotheses: hT