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

State before:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
⊢ ∃ s, A.RowBasis s ∧ s₀ ⊆ s
Tactic:
obtain ⟨s, hss, -, h1,h2⟩ := exists_linearIndependent_extension' hs₀ (subset_univ _)
State after:
case intro.intro.intro.intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ ∃ s, A.RowBasis s ∧ s₀ ⊆ s

State before:
case intro.intro.intro.intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ ∃ s, A.RowBasis s ∧ s₀ ⊆ s
Tactic:
refine ⟨s, ⟨h2, le_antisymm (span_mono ?_) ?_⟩, hss⟩
State after:
case intro.intro.intro.intro.refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun

case intro.intro.intro.intro.refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace

State before:
case intro.intro.intro.intro.refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Tactic:
rw [image_univ, image_eq_range_submatrix] at h1
State after:
case intro.intro.intro.intro.refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : range A ⊆ ↑(span R (range (A.rowSubmatrix s).rowFun))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace

State before:
case intro.intro.intro.intro.refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : range A ⊆ ↑(span R (range (A.rowSubmatrix s).rowFun))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Tactic:
rwa [rowSpace, rowSpace, Submodule.span_le, rowFun]
State after:
no goals

State before:
case intro.intro.intro.intro.refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun
Tactic:
rw [rowFun_rowSubmatrix_eq, range_restrict]
State after:
case intro.intro.intro.intro.refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowFun '' s ⊆ range A.rowFun

State before:
case intro.intro.intro.intro.refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowFun '' s ⊆ range A.rowFun
Tactic:
apply image_subset_range
State after:
no goals