no goals
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type ?u.464024
P2 : Type ?u.464027
V3 : Type ?u.464030
P3 : Type ?u.464033
V4 : Type ?u.464036
P4 : Type ?u.464039
inst✝¹³ : Ring k
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k V4
inst✝¹ : AffineSpace V4 P4
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ ↑(lineMap p₀ p₁) c₁ = ↑(lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
  sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]