ι : Type ?u.995828
ι' : Type ?u.995831
R : Type u_1
R₂ : Type ?u.995837
K : Type ?u.995840
M : Type u_2
M' : Type ?u.995846
M'' : Type ?u.995849
V : Type u
V' : Type ?u.995854
v : ι → M
inst✝⁸ : Ring R
inst✝⁷ : CommRing R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R₂ M
inst✝¹ : Module R M'
inst✝ : Module R M''
c d : R
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R { x // x ∈ N }
hli : ∀ (c : R) (x : M), x ∈ N → c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ↑(let_fun span_b := (_ : span R (Set.range (↑(Submodule.subtype N) ∘ ↑b)) = N);
      Basis.mk (_ : LinearIndependent R (Fin.cons y (↑(Submodule.subtype N) ∘ ↑b)))
        (_ : ∀ (x : M), x ∈ ⊤ → x ∈ span R (Set.range (Fin.cons y (↑(Submodule.subtype N) ∘ ↑b))))) =
    Fin.cons y (Subtype.val ∘ ↑b)
ι : Type ?u.995828
ι' : Type ?u.995831
R : Type u_1
R₂ : Type ?u.995837
K : Type ?u.995840
M : Type u_2
M' : Type ?u.995846
M'' : Type ?u.995849
V : Type u
V' : Type ?u.995854
v : ι → M
inst✝⁸ : Ring R
inst✝⁷ : CommRing R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R₂ M
inst✝¹ : Module R M'
inst✝ : Module R M''
c d : R
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R { x // x ∈ N }
hli : ∀ (c : R) (x : M), x ∈ N → c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ↑(mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ↑b)
unfold mkFinCons
no goals
ι : Type ?u.995828
ι' : Type ?u.995831
R : Type u_1
R₂ : Type ?u.995837
K : Type ?u.995840
M : Type u_2
M' : Type ?u.995846
M'' : Type ?u.995849
V : Type u
V' : Type ?u.995854
v : ι → M
inst✝⁸ : Ring R
inst✝⁷ : CommRing R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R₂ M
inst✝¹ : Module R M'
inst✝ : Module R M''
c d : R
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R { x // x ∈ N }
hli : ∀ (c : R) (x : M), x ∈ N → c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ↑(let_fun span_b := (_ : span R (Set.range (↑(Submodule.subtype N) ∘ ↑b)) = N);
      Basis.mk (_ : LinearIndependent R (Fin.cons y (↑(Submodule.subtype N) ∘ ↑b)))
        (_ : ∀ (x : M), x ∈ ⊤ → x ∈ span R (Set.range (Fin.cons y (↑(Submodule.subtype N) ∘ ↑b))))) =
    Fin.cons y (Subtype.val ∘ ↑b)
exact coe_mk (v := Fin.cons y (N.subtype ∘ b)) _ _