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
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 : t₂ * t₁ = 1
pos : ((t₁ - 1) * (HSub.hSub (α := R) 1 1 / HSub.hSub (α := R) 1 1) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
rw [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
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 : t₂ * t₁ = 1
this : t₁ = 1
⊢ ((t₁ - 1) * (HSub.hSub (α := R) 1 1 / HSub.hSub (α := R) 1 1) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
simp [this]
-- 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 : t₂ * t₁ = 1
pos : t₁ = 1
⊢ ((t₁ - 1) * (HSub.hSub (α := R) 1 1 / HSub.hSub (α := R) 1 1) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
suffices t₁ = 1 by simp [this]
-- 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 : t₂ * t₁ = 1
⊢ t₁ = 1

Tactic:
eq_of_le_of_not_lt ht₁.2 fun ht₁lt =>
        (mul_lt_one_of_nonneg_of_lt_one_right ht₂.2 ht₁.1 ht₁lt).ne h

Premises used: mul_lt_one_of_nonneg_of_lt_one_right, And.right, And.left, eq_of_le_of_not_lt, 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
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 : t₂ * t₁ = 1
⊢ t₁ = 1

Tactic:
exact
      eq_of_le_of_not_lt ht₁.2 fun ht₁lt =>
        (mul_lt_one_of_nonneg_of_lt_one_right ht₂.2 ht₁.1 ht₁lt).ne h

Premises used: mul_lt_one_of_nonneg_of_lt_one_right, And.right, And.left, eq_of_le_of_not_lt, 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
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
neg : ((t₁ - t₂ * t₁) * 1 + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
rw [div_self h]

Premises used: div_self
-- 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₂ * t₁) * 1 + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

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
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
rw : ∀ (h₁ : Wbtw R z x w) (h₂ : Wbtw R z y x), Wbtw R y x w
⊢ Wbtw R w x y

Tactic:
rw [wbtw_comm] at *

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
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R y x w

Tactic:
h₁.trans_left_right h₂

Premises used: Wbtw.trans_left_right
-- 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 z x w
h₂ : Wbtw R z y x
⊢ Wbtw R y x w

Tactic:
exact h₁.trans_left_right h₂

Premises used: Wbtw.trans_left_right
-- 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₁ : Sbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R x y z

Tactic:
⟨h₁.wbtw.trans_left_right h₂.wbtw, h₂.right_ne, h₁.ne_right⟩

Premises used: Sbtw.right_ne, And.intro, Sbtw.wbtw, Sbtw.ne_right, Sbtw, Wbtw.trans_left_right
-- 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₁ : Sbtw R w x z
h₂ : Sbtw R x y z
⊢ Sbtw R w x y

Tactic:
⟨h₁.wbtw.trans_right_left h₂.wbtw, h₁.ne_left, h₂.left_ne⟩

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

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

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

Tactic:
⟨t₁ * t₂ / (1 - t₁ + t₁ * t₂), ?_, ?_⟩

Premises used: affineSegment, HMul.hMul, Set.Mem, Wbtw, setOf, HSub.hSub, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- 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_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
refine_1 : Membership.mem (γ := Set R) (Set.Icc 0 1) (t₁ * t₂ / (1 - t₁ + t₁ * t₂))
refine_2 : (lineMap w z : (a : R) → P) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x
⊢ Wbtw R w x z

Tactic:
refine ⟨t₁ * t₂ / (1 - t₁ + t₁ * t₂), ?_, ?_⟩
-- 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_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
refine_1 : 0 ≤ t₁ * t₂ / (1 - t₁ + t₁ * t₂)
refine_1₁ : t₁ * t₂ / (1 - t₁ + t₁ * t₂) ≤ 1
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (t₁ * t₂ / (1 - t₁ + t₁ * t₂))

Tactic:
constructor
-- 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_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
refine_1 : 0 ≤ 1 - t₁ + t₁ * t₂
⊢ 0 ≤ t₁ * t₂ / (1 - t₁ + t₁ * t₂)

Tactic:
apply div_nonneg (mul_nonneg ht₁.1 ht₂.1)

Premises used: mul_nonneg, And.left, 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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
nlinarith : 1 - t₁ + t₁ * t₂ < 0 → 1 - t₁ + t₁ * t₂ - 0 + (t₁ - 1) + (0 - (0 - t₁) * (0 - t₂)) = 0
⊢ 0 ≤ 1 - t₁ + t₁ * t₂

Tactic:
nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]

Premises used: And.right, And.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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
refine_1 : t₁ * t₂ ≤ 1 - t₁ + t₁ * t₂
refine_1₁ : 0 ≤ 1 - t₁ + t₁ * t₂
⊢ t₁ * t₂ / (1 - t₁ + t₁ * t₂) ≤ 1

Tactic:
apply div_le_one_of_le₀

Premises used: div_le_one_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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ t₁ * t₂ ≤ 1 - t₁ + t₁ * t₂

Tactic:
grind
-- 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_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
contrapose : ∀ (h_ne : 1 - t₁ + t₁ * t₂ = 0), x = y
⊢ 1 - t₁ + t₁ * t₂ ≠ 0

Tactic:
contrapose h_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
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
nlinarith : t₁ < 1 → 1 - t₁ + t₁ * t₂ - 0 + (t₁ - 1) + (0 - (0 - t₁) * (0 - t₂)) = 0
nlinarith₁ : 1 < t₁ → 1 - t₁ + (t₁ - 1) = 0
⊢ t₁ = 1

Tactic:
nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]

Premises used: And.right, And.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
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
⊢ t₁ = 1

Tactic:
have h1 : t₁ = 1 := by nlinarith [ht₁.1, 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 x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
h1 : t₁ = 1
rw : (lineMap w y : (a : R) → P) t₁ = y
rw₁ : (lineMap w y : (a : R) → P) 1 = y
rw₂ rw₃ : y = y
⊢ x = y

Tactic:
rw [← hx, h1, lineMap_apply_one]

Premises used: AffineMap.lineMap_apply_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 x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ 1 - t₁ + t₁ * t₂ ≠ 0

Tactic:
have h_denom : 1 - t₁ + t₁ * t₂ ≠ 0 := by
    contrapose h_ne
    have h1 : t₁ = 1 := by nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
    rw [← hx, h1, lineMap_apply_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 x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
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
⊢ x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)

Tactic:
rw [← hy, lineMap_apply, lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq] at hx

Premises used: eq_comm, AffineMap.lineMap_apply, 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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
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
hx₁ : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) t₂

Tactic:
rw [← hy, lineMap_apply, lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq] at hx

Premises used: eq_comm, AffineMap.lineMap_apply, 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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
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
hx₁ : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₃ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ (lineMap x z : (a : R) → P) t₂ = y

Tactic:
rw [← hy, lineMap_apply, lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq] at hx

Premises used: eq_comm, AffineMap.lineMap_apply, 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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
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
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
⊢ 1 - t₁ + t₁ * t₂ ≠ 0

Tactic:
rw [← hy, lineMap_apply, lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq] at hx

Premises used: eq_comm, AffineMap.lineMap_apply, 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
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 : x -ᵥ w - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
⊢ (lineMap w z : (a : R) → P) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x

Tactic:
rw [lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq, div_eq_mul_inv, mul_comm, mul_smul,
    eq_inv_smul_iff₀ h_denom, add_smul, sub_smul, one_smul]

Premises used: sub_smul, eq_comm, div_eq_mul_inv, one_smul, AffineMap.lineMap_apply, add_smul, mul_comm, eq_inv_smul_iff₀, eq_vadd_iff_vsub_eq, SemigroupAction.mul_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
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) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
⊢ x -ᵥ w - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)

Tactic:
nth_rw 1 [hx]
-- 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_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)
refine_2₉ refine_2₁₀ : (t₁ • t₂) • (z -ᵥ w) = (t₁ • t₂) • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ 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]

Premises used: smul_assoc, vsub_add_vsub_cancel, smul_sub, vsub_sub_vsub_cancel_right, vadd_vsub, SemigroupAction.mul_smul, smul_add
-- 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 x y
h₂ : Wbtw R x y z
h_ne : x ≠ y
⊢ Wbtw R w y z

Tactic:
Wbtw.trans_right (h₁.trans_expand_left h₂ h_ne) h₂

Premises used: Wbtw.trans_expand_left, Wbtw.trans_right
-- 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₁ : Sbtw R w x y
h₂ : Sbtw R x y z
⊢ Sbtw R w x z

Tactic:
⟨Wbtw.trans_expand_left h₁.wbtw h₂.wbtw h₂.left_ne, h₁.left_ne.symm, h₂.left_ne_right⟩

Premises used: Ne.symm, Sbtw.left_ne_right, And.intro, Sbtw.wbtw, Wbtw.trans_expand_left, Sbtw, Sbtw.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
w x y z : P
h₁ : Sbtw R w x y
h₂ : Sbtw R x y z
⊢ Sbtw R w y z

Tactic:
Sbtw.trans_right (h₁.trans_expand_left h₂) h₂

Premises used: Sbtw.trans_expand_left, Sbtw.trans_right
-- 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
h : Wbtw R x y z
⊢ Eq (α := Set P) {y, x, z} {x, y, z}

Tactic:
have : {y, x, z} = {x, y, z} := Set.insert_comm y x {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 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
h : Wbtw R x y z
this : Eq (α := Set P) {y, x, z} {x, y, z}
⊢ Collinear R (P := P) {x, y, z}

Tactic:
simpa [this] using collinear_insert_of_mem_affineSpan_pair (mem_affineSpan h)

Premises used: collinear_insert_of_mem_affineSpan_pair, Wbtw.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 : 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}
⊢ ∃ (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

Premises used: collinear_iff_of_mem, Set.mem_insert
-- 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 : ∃ (v : V), ∀ (p : P), Membership.mem (γ := Set P) {x, y, z} p → ∃ (r : R), p = r • v +ᵥ x
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
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
rcases h with ⟨v, 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
v : V
h : ∀ (p : P), Membership.mem (γ := Set P) {x, y, z} p → ∃ (r : R), p = r • v +ᵥ x
⊢ ∀ (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

Premises used: Set.mem_singleton_iff, Set.mem_insert_iff