[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ ∀ (a b : { v // v ≠ 0 }), Setoid.r a b → Submodule.span K {↑a} = Submodule.span K {↑b}
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨x, rfl : x • b = a⟩
[GOAL]
case mk.mk.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
b : V
hb : b ≠ 0
x : Kˣ
ha : x • b ≠ 0
⊢ Submodule.span K {↑{ val := x • b, property := ha }} = Submodule.span K {↑{ val := b, property := hb }}
[PROOFSTEP]
exact Submodule.span_singleton_group_smul_eq _ x _
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ mk K v hv = mk K w hw ↔ ∃ a, a • w = v
[PROOFSTEP]
rw [mk_eq_mk_iff K v w hv hw]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) ↔ ∃ a, a • w = v
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mp.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v
[PROOFSTEP]
exact ⟨a, ha⟩
[GOAL]
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v
[PROOFSTEP]
refine' ⟨Units.mk0 a fun c => hv.symm _, ha⟩
[GOAL]
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v
[PROOFSTEP]
rwa [c, zero_smul] at ha 
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ Projectivization.submodule v = Submodule.span K {Projectivization.rep v}
[PROOFSTEP]
conv_lhs => rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| Projectivization.submodule v
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| Projectivization.submodule v
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| Projectivization.submodule v
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K { x // x ∈ Projectivization.submodule v } = 1
[PROOFSTEP]
rw [submodule_eq]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K { x // x ∈ Submodule.span K {Projectivization.rep v} } = 1
[PROOFSTEP]
exact finrank_span_singleton v.rep_nonzero
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K { x // x ∈ Projectivization.submodule v }
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K
    { x // x ∈ Projectivization.submodule (mk K (Projectivization.rep v) (_ : Projectivization.rep v ≠ 0)) }
[PROOFSTEP]
change FiniteDimensional K (K ∙ v.rep)
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K { x // x ∈ Submodule.span K {Projectivization.rep v} }
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
h : Projectivization.submodule u = Projectivization.submodule v
⊢ u = v
[PROOFSTEP]
induction' u using ind with u hu
[GOAL]
case h
K : Type u_1
V : Type u_2
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
[PROOFSTEP]
induction' v using ind with v hv
[GOAL]
case h.h
K : Type u_1
V : Type u_2
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
[PROOFSTEP]
rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h 
[GOAL]
case h.h
K : Type u_1
V : Type u_2
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
[PROOFSTEP]
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
⊢ H ∈ Set.range Projectivization.submodule ↔ finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
[PROOFSTEP]
refine ⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
⊢ H ∈ Set.range Projectivization.submodule
[PROOFSTEP]
rcases finrank_eq_one_iff'.1 h with ⟨v : H, hv₀, hv : ∀ w : H, _⟩
[GOAL]
case intro.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
⊢ H ∈ Set.range Projectivization.submodule
[PROOFSTEP]
use mk K (v : V) (Subtype.coe_injective.ne hv₀)
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
⊢ Projectivization.submodule (mk K ↑v (_ : ↑v ≠ ↑0)) = H
[PROOFSTEP]
rw [submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range]
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
⊢ (Set.range fun x => x • ↑v) = ↑H
[PROOFSTEP]
refine (Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
x : V
hx : x ∈ ↑H
⊢ x ∈ Set.range fun x => x • ↑v
[PROOFSTEP]
rcases hv ⟨x, hx⟩ with ⟨c, hc⟩
[GOAL]
case h.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
x : V
hx : x ∈ ↑H
c : K
hc : c • v = { val := x, property := hx }
⊢ x ∈ Set.range fun x => x • ↑v
[PROOFSTEP]
exact ⟨c, congr_arg Subtype.val hc⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
v : { v // v ≠ 0 }
c : ↑f ↑v = 0
⊢ ↑f ↑v = ↑f 0
[PROOFSTEP]
simp [c]
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
⊢ (Setoid.r ⇒ Setoid.r) (fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) fun v =>
    { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }
[PROOFSTEP]
rintro ⟨u, hu⟩ ⟨v, hv⟩ ⟨a, ha⟩
[GOAL]
case mk.mk.intro
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : (fun m => m • ↑{ val := v, property := hv }) a = ↑{ val := u, property := hu }
⊢ Setoid.r ((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := u, property := hu })
    ((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := v, property := hv })
[PROOFSTEP]
use Units.map σ.toMonoidHom a
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : (fun m => m • ↑{ val := v, property := hv }) a = ↑{ val := u, property := hu }
⊢ (fun m => m • ↑((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := v, property := hv }))
      (↑(Units.map ↑σ) a) =
    ↑((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := u, property := hu })
[PROOFSTEP]
dsimp at ha ⊢
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : a • v = u
⊢ ↑(Units.map ↑σ) a • ↑f v = ↑f u
[PROOFSTEP]
erw [← f.map_smulₛₗ, ha]
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u v : ℙ K V
h : map f hf u = map f hf v
⊢ u = v
[PROOFSTEP]
induction' u using ind with u hu
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v : ℙ K V
h✝ : map f hf u✝ = map f hf v
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v
[PROOFSTEP]
induction' v using ind with v hv
[GOAL]
case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : map f hf (mk K u hu) = map f hf (mk K v hv)
⊢ mk K u hu = mk K v hv
[PROOFSTEP]
simp only [map_mk, mk_eq_mk_iff'] at h ⊢
[GOAL]
case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : ∃ a, a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
[PROOFSTEP]
rcases h with ⟨a, ha⟩
[GOAL]
case h.h.intro
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
[PROOFSTEP]
refine ⟨τ a, hf ?_⟩
[GOAL]
case h.h.intro
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ↑f (↑τ a • v) = ↑f u
[PROOFSTEP]
rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
⊢ map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) = id
[PROOFSTEP]
ext ⟨v⟩
[GOAL]
case h.mk
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) (Quot.mk Setoid.r v) = id (Quot.mk Setoid.r v)
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : Field F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
g : W →ₛₗ[τ] U
hg : Function.Injective ↑g
⊢ map (LinearMap.comp g f) (_ : Function.Injective (↑g ∘ fun x => ↑f x)) = map g hg ∘ map f hf
[PROOFSTEP]
ext ⟨v⟩
[GOAL]
case h.mk
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : Field F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
g : W →ₛₗ[τ] U
hg : Function.Injective ↑g
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map (LinearMap.comp g f) (_ : Function.Injective (↑g ∘ fun x => ↑f x)) (Quot.mk Setoid.r v) =
    (map g hg ∘ map f hf) (Quot.mk Setoid.r v)
[PROOFSTEP]
rfl
