-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_iff_left_eq_or_right_mem_image_Ici {x y z : P} :
    Wbtw R x y z ↔ x = y ∨ z ∈ lineMap x y '' Set.Ici (1 : R)

Proof state:
case refine_1
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
x y z : P
h : Wbtw R x y z
⊢ x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1

Tactic:
rcases h with ⟨r, ⟨hr0, hr1⟩, rfl⟩

Result:
case refine_1.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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
⊢ x = (lineMap x z) r ∨ z ∈ ⇑(lineMap x ((lineMap x z) r)) '' Set.Ici 1

Proof state:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z) r ∨ z ∈ ⇑(lineMap x ((lineMap x z) r)) '' Set.Ici 1

Tactic:
rw [Set.mem_image]

Result:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z) r ∨ ∃ x_1 ∈ Set.Ici 1, (lineMap x ((lineMap x z) r)) x_1 = z

Proof state:
case refine_1.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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
⊢ x = (lineMap x z) r ∨ z ∈ ⇑(lineMap x ((lineMap x z) r)) '' Set.Ici 1

Tactic:
rcases hr0.lt_or_eq with (hr0' | rfl)

Result:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z) r ∨ z ∈ ⇑(lineMap x ((lineMap x z) r)) '' Set.Ici 1

case refine_1.intro.intro.intro.inr
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
x z : P
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ x = (lineMap x z) 0 ∨ z ∈ ⇑(lineMap x ((lineMap x z) 0)) '' Set.Ici 1

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
x y z : P
⊢ Wbtw R x y z ↔ x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
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
x y z : P
h : Wbtw R x y z
⊢ x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1

case refine_2
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
x y z : P
h : x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1
⊢ Wbtw R x y z

Proof state:
case refine_2.inr.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
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y ((lineMap x y) r)

Tactic:
refine ⟨r⁻¹, ⟨inv_nonneg.2 (zero_le_one.trans hr), inv_le_one_of_one_le₀ hr⟩, ?_⟩

Result:
case refine_2.inr.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
x y : P
r : R
hr : 1 ≤ r
⊢ (lineMap x ((lineMap x y) r)) r⁻¹ = y

Proof state:
case refine_2.inr.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
x y : P
r : R
hr : 1 ≤ r
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y

Tactic:
rw [inv_mul_cancel₀ (one_pos.trans_le hr).ne', one_smul, vsub_vadd]

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.inr
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
x z : P
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ x = (lineMap x z) 0 ∨ z ∈ ⇑(lineMap x ((lineMap x z) 0)) '' Set.Ici 1

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.inr.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
x y : P
r : R
hr : 1 ≤ r
⊢ (lineMap x ((lineMap x y) r)) r⁻¹ = y

Tactic:
simp only [lineMap_apply, smul_smul, vadd_vsub]

Result:
case refine_2.inr.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
x y : P
r : R
hr : 1 ≤ r
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y

Proof state:
case refine_2.inl
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
x z : P
⊢ Wbtw R x x z

Tactic:
exact wbtw_self_left _ _ _

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z

Tactic:
rw [inv_mul_cancel₀ hr0'.ne', one_smul, vsub_vadd]

Result:
no goals

Proof state:
case refine_2.inr.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
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y ((lineMap x y) r)

Tactic:
rw [Set.mem_Ici] at hr

Result:
case refine_2.inr.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
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y ((lineMap x y) r)

Proof state:
case refine_2
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
x y z : P
h : x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1
⊢ Wbtw R x y z

Tactic:
rcases h with (rfl | ⟨r, ⟨hr, rfl⟩⟩)

Result:
case refine_2.inl
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
x z : P
⊢ Wbtw R x x z

case refine_2.inr.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
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y ((lineMap x y) r)

Proof state:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z) r ∨ ∃ x_1 ∈ Set.Ici 1, (lineMap x ((lineMap x z) r)) x_1 = z

Tactic:
refine .inr ⟨r⁻¹, (one_le_inv₀ hr0').2 hr1, ?_⟩

Result:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (lineMap x ((lineMap x z) r)) r⁻¹ = z

Proof state:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (lineMap x ((lineMap x z) r)) r⁻¹ = z

Tactic:
simp only [lineMap_apply, smul_smul, vadd_vsub]

Result:
case refine_1.intro.intro.intro.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z