case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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
rcases h₁ with ⟨t₁, ht₁, rfl⟩
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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
case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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
rcases h₂ with ⟨t₂, ht₂, rfl⟩
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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₁
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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
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))⟩,
    _⟩
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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₁
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]
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
nth_rw 1 [← mul_one (t₁ - t₂ * t₁)]
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
rw [← mul_sub, mul_div_assoc]
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)

case neg
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
by_cases h : 1 - t₂ * t₁ = 0
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
rw [sub_eq_zero, eq_comm] at h
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
rw [h]
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
suffices t₁ = 1 by simp [this]
no goals
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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
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
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
simp [this]
case neg
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
case neg
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
rw [div_self h]
no goals
case neg
R : Type u_1
V : Type u_2
V' : Type ?u.567237
P : Type u_3
P' : Type ?u.567243
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)
ring_nf