rintro _ ⟨h, l, rfl⟩
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
⊢ N ⊓ LinearMap.range (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) ≤ ⊥
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 R (f ∘ Subtype.val)) l ∈ ↑N
⊢ (Finsupp.total { x // x ∈ ↑t } M R (f ∘ Subtype.val)) l ∈ ⊥