Theorem: Matrix.rank'_transpose (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
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
⊢ Aᵀ.rank' = A.rank'
Tactic:
obtain ⟨s, hs⟩ := A.exists_rowBasis
State after:
case 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
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
⊢ Aᵀ.rank' = A.rank'

State before:
case 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
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
⊢ Aᵀ.rank' = A.rank'
Tactic:
obtain ⟨t, ht⟩ := A.exists_colBasis
State after:
case 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
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
t : Set n
ht : A.ColBasis t
⊢ Aᵀ.rank' = A.rank'

State before:
case 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
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
t : Set n
ht : A.ColBasis t
⊢ Aᵀ.rank' = A.rank'
Tactic:
rw [← ncard_colBasis ht, ← ncard_rowBasis_eq_ncard_colBasis hs ht,
  ← ncard_colBasis hs.colBasis_transpose]
State after:
no goals