exact hs'.ne_zero ⟨0, h₁⟩ (by simp only)
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
h₂ : 0 ∈ f '' ↑t
h₁ : 0 ∈ s
⊢ 0 ∈ ∅
no goals