Theorem: Matrix.rowBases_eq_of_colSpaces_eq (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 : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁.colSpace = A₂.colSpace
⊢ A₁.RowBasis = A₂.RowBasis
Tactic:
ext s
State after:
case h.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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁.colSpace = A₂.colSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s

State before:
case h.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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁.colSpace = A₂.colSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s
Tactic:
rw [← rowSpace_transpose, ← rowSpace_transpose] at h
State after:
case h.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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁ᵀ.rowSpace = A₂ᵀ.rowSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s

State before:
case h.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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁ᵀ.rowSpace = A₂ᵀ.rowSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s
Tactic:
simpa using congr_fun (colBases_eq_of_rowSpaces_eq h) s
State after:
no goals