case h.mk
K : Type u_3
V : Type u_5
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_4
W : Type u_6
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_1
U : Type u_2
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)
K : Type u_3
V : Type u_5
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_4
W : Type u_6
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_1
U : Type u_2
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
ext ⟨v⟩
no goals
case h.mk
K : Type u_3
V : Type u_5
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_4
W : Type u_6
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_1
U : Type u_2
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)
rfl