case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : Wbtw R x y x
⊢ y = x

case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : y = x
⊢ Wbtw R x y x
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
⊢ Wbtw R x y x ↔ y = x
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : Wbtw R x y x
w✝ : R
left✝ : w✝ ∈ Set.Icc 0 1
h₂ : ↑(lineMap x x) w✝ = y
⊢ y = x
case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : Wbtw R x y x
⊢ y = x
have ⟨_, _, h₂⟩ := h
no goals
case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : Wbtw R x y x
w✝ : R
left✝ : w✝ ∈ Set.Icc 0 1
h₂ : ↑(lineMap x x) w✝ = y
⊢ y = x
rw [h₂.symm, lineMap_same_apply]
case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : y = x
⊢ Wbtw R x x x
case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : y = x
⊢ Wbtw R x y x
rw [h]
no goals
case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.153895
P : Type u_3
P' : Type ?u.153901
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y : P
h : y = x
⊢ Wbtw R x x x
exact wbtw_self_left R x x