∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {α : Type u_3}
  (f f_1 : { v // v ≠ 0 } → α) (e_f : f = f_1) (hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b)
  (x x_1 : Projectivization K V), x = x_1 → Projectivization.lift f hf x = Projectivization.lift f_1 ⋯ x_1