Theorem: Basis.toRowMatrix_rowSpace (Matroid/ForMathlib/LinearAlgebra/Matrix/Rowspace.lean)

State before:
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ b.toRowMatrix.rowSpace = U
Tactic:
convert congr_arg (fun (W : Submodule R U) ↦ W.map (Submodule.subtype U)) b.span_eq
State after:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ b.toRowMatrix.rowSpace = map U.subtype (span R (range ⇑b))

case h.e'_3
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ U = map U.subtype ⊤

State before:
case h.e'_3
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ U = map U.subtype ⊤
Tactic:
simp
State after:
no goals

State before:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ b.toRowMatrix.rowSpace = map U.subtype (span R (range ⇑b))
Tactic:
rw [Matrix.rowSpace, map_span]
State after:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ span R (range b.toRowMatrix.rowFun) = span R (⇑U.subtype '' range ⇑b)

State before:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ span R (range b.toRowMatrix.rowFun) = span R (⇑U.subtype '' range ⇑b)
Tactic:
convert rfl
State after:
case h.e'_3.h.e'_6
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ ⇑U.subtype '' range ⇑b = range b.toRowMatrix.rowFun

State before:
case h.e'_3.h.e'_6
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ ⇑U.subtype '' range ⇑b = range b.toRowMatrix.rowFun
Tactic:
ext x
State after:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ x ∈ ⇑U.subtype '' range ⇑b ↔ x ∈ range b.toRowMatrix.rowFun

State before:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ x ∈ ⇑U.subtype '' range ⇑b ↔ x ∈ range b.toRowMatrix.rowFun
Tactic:
simp only [coeSubtype, mem_image, mem_range, exists_exists_eq_and, toRowMatrix]
State after:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ (∃ a, ↑(b a) = x) ↔ ∃ y, (Matrix.of fun i j => ↑(b i) j).rowFun y = x

State before:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ (∃ a, ↑(b a) = x) ↔ ∃ y, (Matrix.of fun i j => ↑(b i) j).rowFun y = x
Tactic:
rfl
State after:
no goals