case inl
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a r : k
⊢ ↑(lineMap (slope f (↑(lineMap a a) r) a) (slope f a (↑(lineMap a a) r))) r = slope f a a

case inr
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ ↑(lineMap (slope f (↑(lineMap a b) r) b) (slope f a (↑(lineMap a b) r))) r = slope f a b
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
⊢ ↑(lineMap (slope f (↑(lineMap a b) r) b) (slope f a (↑(lineMap a b) r))) r = slope f a b
obtain rfl | hab : a = b ∨ a ≠ b := Classical.em _
case inr
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ ↑(lineMap (slope f b (↑(lineMap a b) r)) (slope f (↑(lineMap a b) r) a)) r = slope f b a
case inr
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ ↑(lineMap (slope f (↑(lineMap a b) r) b) (slope f a (↑(lineMap a b) r))) r = slope f a b
rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b]
case h.e'_2.h.e'_6
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ r = (a - ↑(lineMap a b) r) / (a - b)
case inr
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ ↑(lineMap (slope f b (↑(lineMap a b) r)) (slope f (↑(lineMap a b) r) a)) r = slope f b a
convert lineMap_slope_slope_sub_div_sub f b (lineMap a b r) a hab.symm using 2
no goals
case h.e'_2.h.e'_6
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ r = (a - ↑(lineMap a b) r) / (a - b)
rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
  sub_sub_cancel]
no goals
case inl
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a r : k
⊢ ↑(lineMap (slope f (↑(lineMap a a) r) a) (slope f a (↑(lineMap a a) r))) r = slope f a a
simp