exact zero_mem _
case 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
l : { x // x ∈ ↑t } →₀ R
h : (Finsupp.total { x // x ∈ ↑t } (M ⧸ N) R (id ∘ Subtype.val)) l = 0
⊢ 0 ∈ ⊥
no goals