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
h : Wbtw R x y z
hne : z ≠ y
⊢ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x

Tactic:
h.symm.right_mem_image_Ici_of_left_ne hne

Premises used: Wbtw.right_mem_image_Ici_of_left_ne, Wbtw.symm
-- 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 : Wbtw R x y z
hne : z ≠ y
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R {z, y}) x

Tactic:
h.symm.right_mem_affineSpan_of_left_ne hne

Premises used: Wbtw.symm, Wbtw.right_mem_affineSpan_of_left_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
rw :
  Sbtw R z y x ↔
    z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x
rw₁ rw₂ :
  z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x ↔
    z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x
⊢ Sbtw R x y z ↔
    z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x

Tactic:
rw [sbtw_comm, sbtw_iff_left_ne_and_right_mem_image_Ioi]

Premises used: sbtw_iff_left_ne_and_right_mem_image_Ioi, sbtw_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
h : Sbtw R x y z
⊢ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x

Tactic:
h.symm.right_mem_image_Ioi

Premises used: Sbtw.right_mem_image_Ioi, Sbtw.symm
-- 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 : Sbtw R x y z
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R {z, y}) x

Tactic:
h.symm.right_mem_affineSpan

Premises used: Sbtw.symm, Sbtw.right_mem_affineSpan
-- 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 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
s : AffineSubspace R P
hxyz : Wbtw R x y z
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
obtain :
  ∀ (ε : R) (hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P))
    (hxy : x ≠ (lineMap x z : (a : R) → P) ε), z ∈ s
⊢ z ∈ s

Tactic:
obtain ⟨ε, -, rfl⟩ := hxyz

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 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) 0 : P)
hxy : x ≠ (lineMap x z : (a : R) → P) 0
⊢ False

Tactic:
simp at hxy
-- 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 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P)
hxy : x ≠ (lineMap x z : (a : R) → P) ε
⊢ ε ≠ 0

Tactic:
have hε : ε ≠ 0 := by rintro rfl; simp at hxy
-- 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 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P)
hxy : x ≠ (lineMap x z : (a : R) → P) ε
hε : ε ≠ 0
⊢ z ∈ s

Tactic:
simpa [hε] using lineMap_mem ε⁻¹ hx hy

Premises used: AffineMap.lineMap_mem, Inv.inv
-- 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

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

Premises used: affineSegment, div_le_one_of_le₀, Set.Mem, Wbtw, setOf, HDiv.hDiv, And.intro, Exists.intro, Set.image, div_nonneg, LE.le.trans
-- 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
refine : (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Tactic:
refine ⟨r₁ / r₂, ⟨div_nonneg hr₁ (hr₁.trans hr₂), div_le_one_of_le₀ hr₂ (hr₁.trans hr₂)⟩, ?_⟩
-- 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
pos : ∀ (h : r₁ = 0), (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
neg : ∀ (h : ¬r₁ = 0), (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
⊢ (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
by_cases h : r₁ = 0
-- 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
simp [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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : ¬r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
simp [lineMap_apply, smul_smul, ((hr₁.lt_of_ne' h).trans_le hr₂).ne.symm]

Premises used: smul_smul, Ne.symm, AffineMap.lineMap_apply, LT.lt.trans_le, LE.le.lt_of_ne', 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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
inl : ∀ (h : r₁ ≤ r₂), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
inr : ∀ (h : r₂ ≤ r₁), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
rcases le_total r₁ r₂ with (h | h)

Premises used: le_total
-- 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
Or.inl (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₁ h)

Premises used: wbtw_smul_vadd_smul_vadd_of_nonneg_of_le, 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inl (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₁ h)

Premises used: wbtw_smul_vadd_smul_vadd_of_nonneg_of_le, 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₂ h)

Premises used: wbtw_smul_vadd_smul_vadd_of_nonneg_of_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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₂ h)

Premises used: wbtw_smul_vadd_smul_vadd_of_nonneg_of_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
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
⊢ Wbtw R x (-r₁ • -v +ᵥ x) (-r₂ • -v +ᵥ x)

Tactic:
wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x (-v) (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_neg_iff.2 hr₂)

Premises used: Iff.mpr, wbtw_smul_vadd_smul_vadd_of_nonneg_of_le, Neg.neg, Left.nonneg_neg_iff, neg_le_neg_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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
h : r₁ • v +ᵥ x = -r₁ • -v +ᵥ x
h₁ : r₂ • v +ᵥ x = -r₂ • -v +ᵥ x
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Tactic:
convert!
    wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x (-v) (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_neg_iff.2 hr₂) using
    1

Premises used: Iff.mpr, wbtw_smul_vadd_smul_vadd_of_nonneg_of_le, Neg.neg, Left.nonneg_neg_iff, neg_le_neg_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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
h h₁ : r₁ • v +ᵥ x = r₁ • v +ᵥ x
⊢ r₁ • v +ᵥ x = -r₁ • -v +ᵥ x

Tactic:
rw [neg_smul_neg]

Premises used: neg_smul_neg
-- 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
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
h h₁ : r₂ • v +ᵥ x = r₂ • v +ᵥ x
⊢ r₂ • v +ᵥ x = -r₂ • -v +ᵥ x

Tactic:
rw [neg_smul_neg]

Premises used: neg_smul_neg
-- 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
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
inl : ∀ (h : r₁ ≤ r₂), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
inr : ∀ (h : r₂ ≤ r₁), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
rcases le_total r₁ r₂ with (h | h)

Premises used: le_total
-- 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
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₂ h)

Premises used: wbtw_smul_vadd_smul_vadd_of_nonpos_of_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
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₂ h)

Premises used: wbtw_smul_vadd_smul_vadd_of_nonpos_of_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
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
Or.inl (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₁ h)

Premises used: Or.inl, wbtw_smul_vadd_smul_vadd_of_nonpos_of_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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inl (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₁ h)

Premises used: Or.inl, wbtw_smul_vadd_smul_vadd_of_nonpos_of_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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
⊢ Wbtw R (r₁ • v +ᵥ x) (-r₁ • v +ᵥ r₁ • v +ᵥ x) ((r₂ - r₁) • v +ᵥ r₁ • v +ᵥ x)

Tactic:
wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (r₁ • v +ᵥ x) v (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_sub_iff_le_add.2 ((le_add_iff_nonneg_left r₁).2 hr₂))

Premises used: Iff.mpr, HVAdd.hVAdd, wbtw_smul_vadd_smul_vadd_of_nonneg_of_le, HSMul.hSMul, neg_le_sub_iff_le_add, le_add_iff_nonneg_left, Left.nonneg_neg_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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
h : x = -r₁ • v +ᵥ r₁ • v +ᵥ x
h₁ : r₂ • v +ᵥ x = (r₂ - r₁) • v +ᵥ r₁ • v +ᵥ x
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Tactic:
convert!
    wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (r₁ • v +ᵥ x) v (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_sub_iff_le_add.2 ((le_add_iff_nonneg_left r₁).2 hr₂)) using
    1

Premises used: Iff.mpr, HVAdd.hVAdd, wbtw_smul_vadd_smul_vadd_of_nonneg_of_le, HSMul.hSMul, neg_le_sub_iff_le_add, le_add_iff_nonneg_left, Left.nonneg_neg_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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
⊢ x = -r₁ • v +ᵥ r₁ • v +ᵥ x

Tactic:
simp [sub_smul, ← add_vadd]

Premises used: AddSemigroupAction.add_vadd, sub_smul
-- 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
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
⊢ r₂ • v +ᵥ x = (r₂ - r₁) • v +ᵥ r₁ • v +ᵥ x

Tactic:
simp [sub_smul, ← add_vadd]

Premises used: AddSemigroupAction.add_vadd, sub_smul
-- 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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
rw : Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Tactic:
rw [wbtw_comm]

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
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)

Tactic:
wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg x v hr₂ hr₁

Premises used: wbtw_smul_vadd_smul_vadd_of_nonpos_of_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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)

Tactic:
exact wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg x v hr₂ hr₁

Premises used: wbtw_smul_vadd_smul_vadd_of_nonpos_of_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
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
rcases :
  ∀ (t₁ : R) (ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁) (h₂ : Wbtw R w x ((lineMap w z : (a : R) → P) t₁)),
    Wbtw R x ((lineMap w z : (a : R) → P) t₁) z
⊢ Wbtw R x y z

Tactic:
rcases h₁ with ⟨t₁, ht₁, 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
w x z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
h₂ : Wbtw R w x ((lineMap w z : (a : R) → P) t₁)
rcases :
  ∀ (t₂ : R) (ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂),
    Wbtw R ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) ((lineMap w z : (a : R) → P) t₁) z
⊢ Wbtw R x ((lineMap w z : (a : R) → P) t₁) z

Tactic:
rcases h₂ with ⟨t₂, ht₂, 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ Wbtw R ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) ((lineMap w z : (a : R) → P) t₁) z

Tactic:
⟨(t₁ - t₂ * t₁) / (1 - t₂ * t₁),
      ⟨div_nonneg (sub_nonneg.2 (mul_le_of_le_one_left ht₁.1 ht₂.2))
          (sub_nonneg.2 (mul_le_one₀ ht₂.2 ht₁.1 ht₁.2)), div_le_one_of_le₀
            (sub_le_sub_right ht₁.2 _) (sub_nonneg.2 (mul_le_one₀ ht₂.2 ht₁.1 ht₁.2))⟩,
      ?_⟩

Premises used: affineSegment, div_le_one_of_le₀, sub_le_sub_right, Iff.mpr, HMul.hMul, Set.Mem, Wbtw, setOf, HSub.hSub, HDiv.hDiv, mul_le_of_le_one_left, And.right, And.left, mul_le_one₀, And.intro, Exists.intro, Set.image, div_nonneg, OfNat.ofNat, sub_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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
t₃ :
  Eq.{u_4 + 1} (α := P)
    (((lineMap ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) z : R →ᵃ[R] P) : (a : R) → P)
        ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) :
      P)
    ((lineMap w z : (a : R) → P) t₁ : P)
⊢ Wbtw R ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) ((lineMap w z : (a : R) → P) t₁) z

Tactic:
refine
    ⟨(t₁ - t₂ * t₁) / (1 - t₂ * t₁),
      ⟨div_nonneg (sub_nonneg.2 (mul_le_of_le_one_left ht₁.1 ht₂.2))
          (sub_nonneg.2 (mul_le_one₀ ht₂.2 ht₁.1 ht₁.2)), div_le_one_of_le₀
            (sub_le_sub_right ht₁.2 _) (sub_nonneg.2 (mul_le_one₀ ht₂.2 ht₁.1 ht₁.2))⟩,
      ?_⟩
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
simp : ((t₁ - t₂ * t₁ - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
⊢ Eq.{u_4 + 1} (α := P)
    (((lineMap ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) z : R →ᵃ[R] P) : (a : R) → P)
        ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) :
      P)
    ((lineMap w z : (a : R) → P) t₁ : P)

Tactic:
simp only [lineMap_apply, smul_smul, ← add_vadd, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul,
    ← add_smul, vadd_vsub, vadd_right_cancel_iff, div_mul_eq_mul_div, div_sub_div_same]

Premises used: vsub_vadd_eq_vsub_sub, AddSemigroupAction.add_vadd, sub_smul, smul_smul, div_mul_eq_mul_div, AffineMap.lineMap_apply, smul_sub, add_smul, div_sub_div_same, vadd_vsub, vadd_right_cancel_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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
nth_rw : (((t₁ - t₂ * t₁) * 1 - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
⊢ ((t₁ - t₂ * t₁ - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
nth_rw 1 [← mul_one (t₁ - t₂ * t₁)]

Premises used: HMul.hMul, HSub.hSub, mul_one
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
rw : ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
⊢ (((t₁ - t₂ * t₁) * 1 - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
rw [← mul_sub, mul_div_assoc]

Premises used: mul_sub, mul_div_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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
pos : ∀ (h : 1 - t₂ * t₁ = 0), ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
neg : ∀ (h : ¬1 - t₂ * t₁ = 0), ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
by_cases h : 1 - t₂ * t₁ = 0
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
h : 1 - t₂ * t₁ = 0
⊢ t₂ * t₁ = 1

Tactic:
rw [sub_eq_zero, eq_comm] at h

Premises used: sub_eq_zero, eq_comm