case h
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v : ℙ K V
h✝ : Projectivization.submodule u✝ = Projectivization.submodule v
u : V
hu : u ≠ 0
h : Projectivization.submodule (mk K u hu) = Projectivization.submodule v
⊢ mk K u hu = v
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
h : Projectivization.submodule u = Projectivization.submodule v
⊢ u = v
induction' u using ind with u hu
case h.h
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v✝ : ℙ K V
h✝² : Projectivization.submodule u✝ = Projectivization.submodule v✝
u : V
hu : u ≠ 0
h✝¹ : Projectivization.submodule (mk K u hu) = Projectivization.submodule v✝
v : V
hv : v ≠ 0
h✝ : Projectivization.submodule u✝ = Projectivization.submodule (mk K v hv)
h : Projectivization.submodule (mk K u hu) = Projectivization.submodule (mk K v hv)
⊢ mk K u hu = mk K v hv
case h
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v : ℙ K V
h✝ : Projectivization.submodule u✝ = Projectivization.submodule v
u : V
hu : u ≠ 0
h : Projectivization.submodule (mk K u hu) = Projectivization.submodule v
⊢ mk K u hu = v
induction' v using ind with v hv
case h.h
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v✝ : ℙ K V
h✝² : Projectivization.submodule u✝ = Projectivization.submodule v✝
u : V
hu : u ≠ 0
h✝¹ : Projectivization.submodule (mk K u hu) = Projectivization.submodule v✝
v : V
hv : v ≠ 0
h✝ : Projectivization.submodule u✝ = Projectivization.submodule (mk K v hv)
h : ∃ z, z • u = v
⊢ mk K u hu = mk K v hv
case h.h
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v✝ : ℙ K V
h✝² : Projectivization.submodule u✝ = Projectivization.submodule v✝
u : V
hu : u ≠ 0
h✝¹ : Projectivization.submodule (mk K u hu) = Projectivization.submodule v✝
v : V
hv : v ≠ 0
h✝ : Projectivization.submodule u✝ = Projectivization.submodule (mk K v hv)
h : Projectivization.submodule (mk K u hu) = Projectivization.submodule (mk K v hv)
⊢ mk K u hu = mk K v hv
rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
no goals
case h.h
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v✝ : ℙ K V
h✝² : Projectivization.submodule u✝ = Projectivization.submodule v✝
u : V
hu : u ≠ 0
h✝¹ : Projectivization.submodule (mk K u hu) = Projectivization.submodule v✝
v : V
hv : v ≠ 0
h✝ : Projectivization.submodule u✝ = Projectivization.submodule (mk K v hv)
h : ∃ z, z • u = v
⊢ mk K u hu = mk K v hv
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm