Theorem: Matrix.rowBasis_iff_maximal_linearIndependent (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.RowBasis s ↔ s ∈ maximals (fun x x_1 => x ⊆ x_1) {b | LinearIndependent (ι := ↑b) R (A.rowSubmatrix b).rowFun}
Tactic:
rw [mem_maximals_setOf_iff, RowBasis, and_congr_right_iff]
State after:
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
⊢ LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun →
    ((A.rowSubmatrix s).rowSpace = A.rowSpace ↔
      ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y)

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
⊢ LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun →
    ((A.rowSubmatrix s).rowSpace = A.rowSpace ↔
      ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y)
Tactic:
refine fun hli ↦ ⟨fun h y hy hsy ↦ hsy.antisymm fun e he ↦ by_contra fun hes ↦ ?_,
    fun h ↦ le_antisymm (span_mono ?_) ?_⟩
State after:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
⊢ False

case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun

case refine_3
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace

State before:
case refine_3
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Tactic:
rintro x hx
State after:
case refine_3
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
x : n → R
hx : x ∈ A.rowSpace
⊢ x ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
x : n → R
hx : x ∈ A.rowSpace
⊢ x ∈ (A.rowSubmatrix s).rowSpace
Tactic:
obtain ⟨k, c, f, g, rfl⟩ := mem_span_set'.1 hx
State after:
case refine_3.intro.intro.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∑ i : Fin k, c i • ↑(f i) ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3.intro.intro.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∑ i : Fin k, c i • ↑(f i) ∈ (A.rowSubmatrix s).rowSpace
Tactic:
apply sum_smul_mem
State after:
case refine_3.intro.intro.intro.refl.hyp
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∀ c ∈ Finset.univ, ↑(f c) ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3.intro.intro.intro.refl.hyp
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∀ c ∈ Finset.univ, ↑(f c) ∈ (A.rowSubmatrix s).rowSpace
Tactic:
rintro i -
State after:
case refine_3.intro.intro.intro.refl.hyp
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
⊢ ↑(f i) ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3.intro.intro.intro.refl.hyp
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
⊢ ↑(f i) ∈ (A.rowSubmatrix s).rowSpace
Tactic:
obtain ⟨_,⟨j,hj,rfl⟩⟩ := f i
State after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
⊢ ↑⟨A.rowFun j, ⋯⟩ ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
⊢ ↑⟨A.rowFun j, ⋯⟩ ∈ (A.rowSubmatrix s).rowSpace
Tactic:
simp only
State after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Tactic:
obtain (hjs | hjs) := em (j ∈ s)
State after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∈ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace

case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Tactic:
by_contra hsp
State after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
⊢ False

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
⊢ False
Tactic:
have heq := (h <| (linearIndependent_insert' hjs).2 ⟨hli, fun hsp' ↦ hsp ?_⟩) (subset_insert _ _)
State after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
heq : s = insert j s
⊢ False

case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
hsp' : A j ∈ span R (A '' s)
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
hsp' : A j ∈ span R (A '' s)
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Tactic:
rwa [image_eq_range_submatrix, span_eq_rowSpace ] at hsp'
State after:
no goals

State before:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
⊢ False
Tactic:
have hse : LinearIndependent R (A.rowSubmatrix (insert e s)) := by
  apply hy.comp (inclusion (insert_subset he hsy)) <| inclusion_injective _
State after:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ False

State before:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ False
Tactic:
apply ((linearIndependent_insert' hes).1 hse).2
State after:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ A e ∈ span R (A '' s)

State before:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ A e ∈ span R (A '' s)
Tactic:
have hsp := h.symm.le.subset <| (subset_span <| mem_range_self _   : A e ∈ _)
State after:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
hsp : A e ∈ ↑(A.rowSubmatrix s).rowSpace
⊢ A e ∈ span R (A '' s)

State before:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
hsp : A e ∈ ↑(A.rowSubmatrix s).rowSpace
⊢ A e ∈ span R (A '' s)
Tactic:
rwa [image_eq_range_submatrix, span_eq_rowSpace]
State after:
no goals

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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
⊢ LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
Tactic:
apply hy.comp (inclusion (insert_subset he hsy)) <| inclusion_injective _
State after:
no goals

State before:
case 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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun
Tactic:
rintro _ ⟨x, -, rfl⟩
State after:
case refine_2.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
x : ↑s
⊢ (A.rowSubmatrix s).rowFun x ∈ range A.rowFun

State before:
case refine_2.intro.refl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
x : ↑s
⊢ (A.rowSubmatrix s).rowFun x ∈ range A.rowFun
Tactic:
exact ⟨x, rfl⟩
State after:
no goals

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∈ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Tactic:
apply subset_span
State after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∈ s
⊢ A.rowFun j ∈ range (A.rowSubmatrix s).rowFun

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∈ s
⊢ A.rowFun j ∈ range (A.rowSubmatrix s).rowFun
Tactic:
simp only [rowFun_rowSubmatrix_eq, range_restrict, mem_image]
State after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∈ s
⊢ ∃ x ∈ s, A.rowFun x = A.rowFun j

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∈ s
⊢ ∃ x ∈ s, A.rowFun x = A.rowFun j
Tactic:
exact ⟨j,hjs,rfl⟩
State after:
no goals

State before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
heq : s = insert j s
⊢ False
Tactic:
exact hjs (heq.symm.subset (mem_insert _ _))
State after:
no goals