awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ ∃ (r : R), y = r • v +ᵥ x

Tactic:
have hy := h y (Or.inr (Or.inl rfl))
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ ∃ (r : R), z = r • v +ᵥ x

Tactic:
have hz := h z (Or.inr (Or.inr rfl))
-- Module: Mathlib.Analysis.Convex.Between
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
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)
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
rcases hy with ⟨ty, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
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
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)
⊢ Wbtw R x (ty • v +ᵥ x) z ∨ Wbtw R (ty • v +ᵥ x) z x ∨ Wbtw R z x (ty • v +ᵥ x)

Tactic:
rcases hz with ⟨tz, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
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)
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)
⊢ 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)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.Convex.Between
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)
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)
⊢ 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)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.Convex.Between
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
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)
⊢ 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:
rw [wbtw_comm (z := x)]

Premises used: wbtw_comm
-- Module: Mathlib.Analysis.Convex.Between
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
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)
⊢ 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]

Premises used: or_assoc
-- Module: Mathlib.Analysis.Convex.Between
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)

Tactic:
Or.inl (wbtw_or_wbtw_smul_vadd_of_nonpos _ _ hy0.le hz0.le)

Premises used: LT.lt.le, Or.inl, wbtw_or_wbtw_smul_vadd_of_nonpos
-- Module: Mathlib.Analysis.Convex.Between
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)

Tactic:
exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonpos _ _ hy0.le hz0.le)

Premises used: LT.lt.le, Or.inl, wbtw_or_wbtw_smul_vadd_of_nonpos
-- Module: Mathlib.Analysis.Convex.Between
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 : R
hy0 : ty < 0
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:
simp
-- Module: Mathlib.Analysis.Convex.Between
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 : 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:
Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos _ _ hz0.le hy0.le))

Premises used: LT.lt.le, Or.inr, wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos
-- Module: Mathlib.Analysis.Convex.Between
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 : 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:
exact Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos _ _ hz0.le hy0.le))

Premises used: LT.lt.le, Or.inr, wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos
-- Module: Mathlib.Analysis.Convex.Between
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
tz : R
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:
simp
-- Module: Mathlib.Analysis.Convex.Between
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)
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)
⊢ 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)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.Convex.Between
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 : 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:
Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg _ _ hz0.le hy0.le))

Premises used: wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg, LT.lt.le, Or.inr
-- Module: Mathlib.Analysis.Convex.Between
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 : 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:
refine Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg _ _ hz0.le hy0.le))

Premises used: wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg, LT.lt.le, Or.inr
-- Module: Mathlib.Analysis.Convex.Between
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 : R
hy0 : 0 < ty
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:
simp
-- Module: Mathlib.Analysis.Convex.Between
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
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)
⊢ 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:
rw [wbtw_comm (z := x)]

Premises used: wbtw_comm
-- Module: Mathlib.Analysis.Convex.Between
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
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)
⊢ 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]

Premises used: or_assoc
-- Module: Mathlib.Analysis.Convex.Between
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)

Tactic:
Or.inl (wbtw_or_wbtw_smul_vadd_of_nonneg _ _ hy0.le hz0.le)

Premises used: LT.lt.le, wbtw_or_wbtw_smul_vadd_of_nonneg, Or.inl
-- Module: Mathlib.Analysis.Convex.Between
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)

Tactic:
exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonneg _ _ hy0.le hz0.le)

Premises used: LT.lt.le, wbtw_or_wbtw_smul_vadd_of_nonneg, Or.inl
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y)

Tactic:
simp [← wbtw_vsub_const_iff x, ← mem_segment_iff_wbtw, mem_segment_iff_sameRay]

Premises used: mem_segment_iff_sameRay, mem_segment_iff_wbtw, wbtw_vsub_const_iff
-- Module: Mathlib.Analysis.Convex.Between
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
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
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
rcases h with (h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩)
-- Module: Mathlib.Analysis.Convex.Between
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 : y -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Between
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 : z -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Between
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
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
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
wlog hr : r₂ ≤ r₁ generalizing r₁ r₂ y z
-- Module: Mathlib.Analysis.Convex.Between
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₁
inr : Wbtw R x z y ∨ Wbtw R x y z
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
rw [or_comm]

Premises used: or_comm
-- Module: Mathlib.Analysis.Convex.Between
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 z y ∨ Wbtw R x y z

Tactic:
apply this r₂ r₁ hr₂ hr₁ h.symm (Std.le_of_not_ge hr)

Premises used: Eq.symm, Std.le_of_not_ge
-- Module: Mathlib.Analysis.Convex.Between
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₁ : Wbtw R x y z
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
left
-- Module: Mathlib.Analysis.Convex.Between
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

Tactic:
⟨r₂ / r₁, ⟨div_nonneg hr₂.le hr₁.le, div_le_one_of_le₀ hr hr₁.le⟩, ?_⟩

Premises used: affineSegment, div_le_one_of_le₀, Set.Mem, Wbtw, setOf, HDiv.hDiv, LT.lt.le, And.intro, Exists.intro, Set.image, div_nonneg
-- Module: Mathlib.Analysis.Convex.Between
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₁ : (lineMap x z : (a : R) → P) (r₂ / r₁) = y
⊢ Wbtw R x y z

Tactic:
refine ⟨r₂ / r₁, ⟨div_nonneg hr₂.le hr₁.le, div_le_one_of_le₀ hr hr₁.le⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
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₁
⊢ y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x

Tactic:
simp [← h, hr₁.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Between
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₁
⊢ y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x

Tactic:
have h' : y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x := by simp [← h, hr₁.ne']
-- Module: Mathlib.Analysis.Convex.Between
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
h₁ : (r₂ / r₁) • (z -ᵥ x) = (r₁⁻¹ * r₂) • (z -ᵥ x)
⊢ (lineMap x z : (a : R) → P) (r₂ / r₁) = y

Tactic:
simp only [lineMap_apply, h', vadd_vsub_assoc, smul_smul, eq_vadd_iff_vsub_eq, vsub_self,
    add_zero]

Premises used: vadd_vsub_assoc, smul_smul, AffineMap.lineMap_apply, add_zero, vsub_self, eq_vadd_iff_vsub_eq
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ (r₂ / r₁) • (z -ᵥ x) = (r₁⁻¹ * r₂) • (z -ᵥ x)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Convex.Between
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 (ι := 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) → ι))
⊢ ¬Collinear R
      (Set.range (ι := Fin 3)
        (T ∘
          (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } :
            (a : Fin (Nat.succ 0).succ.succ) → ι)))

Tactic:
rw [affineIndependent_iff_not_collinear] at hT

Premises used: affineIndependent_iff_not_collinear
-- Module: Mathlib.Analysis.Convex.Between
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 :
  ¬Collinear R
      (Set.range (ι := Fin 3)
        (T ∘
          (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } :
            (a : Fin (Nat.succ 0).succ.succ) → ι)))
contrapose :
  ∀ (hT : Wbtw R (T i) (T j) (T k)),
    Collinear R
      (Set.range (ι := Fin 3)
        (T ∘
          (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } :
            (a : Fin (Nat.succ 0).succ.succ) → ι)))
⊢ ¬Wbtw R (T i) (T j) (T k)

Tactic:
contrapose hT