-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_left_right {w x y z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) :
    Wbtw R x y z

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (lineMap ((lineMap w ((lineMap w z) t₁)) t₂) z) ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) = (lineMap w z) t₁

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]

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ((t₁ - t₂ * t₁ - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x ((lineMap w z) t₁)
⊢ Wbtw R x ((lineMap w z) t₁) z

Tactic:
rcases h₂ with ⟨t₂, ht₂, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ Wbtw R ((lineMap w ((lineMap w z) t₁)) t₂) ((lineMap w z) t₁) z

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
rw [h]

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
⊢ ((t₁ - 1) * ((1 - 1) / (1 - 1)) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ((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₁)]

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (((t₁ - t₂ * t₁) * 1 - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R x y z

Tactic:
rcases h₁ with ⟨t₁, ht₁, rfl⟩

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x ((lineMap w z) t₁)
⊢ Wbtw R x ((lineMap w z) t₁) z

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ Wbtw R ((lineMap w ((lineMap w z) t₁)) t₂) ((lineMap w z) 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))⟩,
    ?_⟩

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (lineMap ((lineMap w ((lineMap w z) t₁)) t₂) z) ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) = (lineMap w z) t₁

Proof state:
case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * 1 + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
ring_nf

Result:
no goals

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : 1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
rw [sub_eq_zero, eq_comm] at h

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Proof state:
case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
rw [div_self h]

Result:
case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * 1 + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
this : t₁ = 1
⊢ ((t₁ - 1) * ((1 - 1) / (1 - 1)) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
simp [this]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (((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]

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
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

Result:
no goals