awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
v : n → R
⊢ ∃ (a : n → R), (A.mulVecLin : (a : n → R) → n → R) a = v

Tactic:
exact ⟨(A⁻¹).mulVecLin v, by simp [mul_nonsing_inv _ hA]⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ IsUnit A.det

Tactic:
hA
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
h : (LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin = A
⊢ IsUnit.{uR} (M := R)
    (det.{uR, um} (n := m) ((LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin))

Tactic:
convert! hA
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
h :
  Eq (α := (m → R) →ₗ[R] m → R) A.mulVecLin
    (((LinearMap.toMatrix b b).symm : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) A)
⊢ (LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin = A

Tactic:
rw [← LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ Eq (α := (m → R) →ₗ[R] m → R) A.mulVecLin
    (((LinearMap.toMatrix b b).symm : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) A)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ IsUnit.{uR} (M := R)
    (det.{uR, um} (n := m) ((LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin))

Tactic:
replace hA : IsUnit (LinearMap.toMatrix b b A.mulVecLin).det := by
    convert! hA; rw [← LinearEquiv.eq_symm_apply]; rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA :
  IsUnit.{uR} (M := R)
    (det.{uR, um} (n := m) ((LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin))
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA :
  IsUnit.{uR} (M := R)
    (det.{uR, um} (n := m) ((LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin))
x : n → R
x_1 : m
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA :
  IsUnit.{uR} (M := R)
    (det.{uR, um} (n := m) ((LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have hAB : mulVecLin (A * B) = (LinearEquiv.ofIsUnitDet hA).comp (mulVecLin B) := by ext; simp
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
⊢ Module.Finite R ↥(span R (range (A.submatrix r id).col))

Tactic:
have := Module.Finite.span_of_finite R (Set.finite_range (A.submatrix r id).col)
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ (A.submatrix r c).rank = ((A.submatrix r id)ᵀᵀ.submatrix id c)ᵀᵀ.rank

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
rw :
  finrank R ↥(span R (range ((A.submatrix r id).submatrix id c).col)) ≤
    finrank R ↥(span R (range (A.submatrix r id).col))
⊢ ((A.submatrix r id)ᵀᵀ.submatrix id c)ᵀᵀ.rank ≤ finrank R ↥(span R (range (A.submatrix r id).col))

Tactic:
rw [rank, Matrix.mulVecLin_transpose, Matrix.transpose_submatrix, transpose_transpose,
        range_vecMulLinear, ← Matrix.transpose_submatrix, row_transpose]

Premises used: Matrix.transpose_submatrix, range_vecMulLinear, Matrix.transpose_transpose, Matrix.rank, Matrix.row_transpose, Matrix.mulVecLin_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(span R (range ((A.submatrix r id).submatrix id c).col)) ≤
    finrank R ↥(span R (range (A.submatrix r id).col))

Tactic:
Submodule.finrank_mono (Submodule.span_mono (fun v ⟨j, hj⟩ => ⟨c j, hj⟩))

Premises used: _private.0.Matrix.rank_submatrix_le.match_1, Matrix.submatrix, Set.Mem, Membership.mem, id, Submodule.span_mono, Submodule.finrank_mono, Exists.intro, Set.range, Matrix.col
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(span R (range ((A.submatrix r id).submatrix id c).col)) ≤
    finrank R ↥(span R (range (A.submatrix r id).col))

Tactic:
exact Submodule.finrank_mono (Submodule.span_mono (fun v ⟨j, hj⟩ => ⟨c j, hj⟩))
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
rw : finrank R ↥(span R (range (A.submatrix r id).col)) = finrank R ↥(span R (range (A.submatrix r id)ᵀ.row))
⊢ finrank R ↥(span R (range (A.submatrix r id).col)) = (A.submatrix r id)ᵀᵀ.rank

Tactic:
rw [rank, Matrix.mulVecLin_transpose, range_vecMulLinear]

Premises used: range_vecMulLinear, Matrix.rank, Matrix.mulVecLin_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(span R (range (A.submatrix r id).col)) = finrank R ↥(span R (range (A.submatrix r id)ᵀ.row))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ (A.submatrix r id)ᵀᵀ.rank = rank (n := n) (A.submatrix r (⇑(Equiv.refl n) : (a : n) → n))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
calc : rank (n := n) (A.submatrix r (⇑(Equiv.refl n) : (a : n) → n)) ≤ A.rank
⊢ (A.submatrix r c).rank ≤ A.rank

Tactic:
calc
    _ = (((A.submatrix r id)ᵀᵀ.submatrix id c)ᵀᵀ).rank := by simp
    _ ≤ finrank R (span R (range (A.submatrix r id).col)) := by
      rw [rank, Matrix.mulVecLin_transpose, Matrix.transpose_submatrix, transpose_transpose,
        range_vecMulLinear, ← Matrix.transpose_submatrix, row_transpose]
      exact Submodule.finrank_mono (Submodule.span_mono (fun v ⟨j, hj⟩ => ⟨c j, hj⟩))
    _ = (A.submatrix r id)ᵀᵀ.rank := by
      rw [rank, Matrix.mulVecLin_transpose, range_vecMulLinear]
      rfl
    _ = (A.submatrix r (Equiv.refl n)).rank := by simp

Premises used: Matrix.submatrix, Membership.mem, Matrix.rank, id, Subtype, Matrix.transpose, Submodule.span, Set.range, Matrix.col, Equiv.refl, DFunLike.coe, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
calc :
  finrank R ↥(Submodule.map (LinearMap.funLeft R R r) (LinearMap.range A.mulVecLin)) ≤
    finrank R ↥(LinearMap.range A.mulVecLin)
⊢ rank (n := n) (A.submatrix r (⇑(Equiv.refl n) : (a : n) → n)) ≤ A.rank

Tactic:
rw [rank, rank, mulVecLin_submatrix, LinearMap.range_comp, LinearMap.range_comp,
    show LinearMap.funLeft R R (Equiv.refl n).symm = LinearEquiv.funCongrLeft R R
      (Equiv.refl n).symm from rfl, LinearEquiv.range, Submodule.map_top]

Premises used: Submodule.map_top, LinearMap.range_comp, Matrix.rank, Matrix.mulVecLin_submatrix, rfl, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R r) (LinearMap.range A.mulVecLin)) ≤
    finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
Submodule.finrank_map_le _ _

Premises used: Set.Mem, Submodule.finrank_map_le
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R r) (LinearMap.range A.mulVecLin)) ≤
    finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
exact Submodule.finrank_map_le _ _

Premises used: Submodule.finrank_map_le
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
em : m ≃ m₀
en : n ≃ n₀
A : Matrix m n R
rw :
  finrank R ↥(LinearMap.range (M := n₀ → R) (mulVecLin ((reindex em en : (a : Matrix m n R) → Matrix m₀ n₀ R) A))) =
    A.rank
rw₁ :
  finrank R ↥(LinearMap.range (M := n₀ → R) (mulVecLin ((reindex em en : (a : Matrix m n R) → Matrix m₀ n₀ R) A))) =
    finrank R ↥(LinearMap.range A.mulVecLin)
rw₂ :
  finrank R
      ↥((↑(LinearEquiv.funCongrLeft R R em.symm) : (m → R) →ₗ[R] m₀ → R) ∘ₗ
            A.mulVecLin ∘ₗ (↑(LinearEquiv.funCongrLeft R R en) : (n₀ → R) →ₗ[R] n → R)).range =
    finrank R ↥(LinearMap.range A.mulVecLin)
rw₃ :
  finrank R
      ↥(Submodule.map (↑(LinearEquiv.funCongrLeft R R em.symm) : (m → R) →ₗ[R] m₀ → R)
          (A.mulVecLin ∘ₗ (↑(LinearEquiv.funCongrLeft R R en) : (n₀ → R) →ₗ[R] n → R)).range) =
    finrank R ↥(LinearMap.range A.mulVecLin)
rw₄ :
  finrank R
      ↥(Submodule.map (↑(LinearEquiv.funCongrLeft R R em.symm) : (m → R) →ₗ[R] m₀ → R)
          (Submodule.map A.mulVecLin (LinearMap.range (↑(LinearEquiv.funCongrLeft R R en) : (n₀ → R) →ₗ[R] n → R)))) =
    finrank R ↥(LinearMap.range A.mulVecLin)
rw₅ :
  finrank R
      ↥(Submodule.map (↑(LinearEquiv.funCongrLeft R R em.symm) : (m → R) →ₗ[R] m₀ → R) (Submodule.map A.mulVecLin ⊤)) =
    finrank R ↥(LinearMap.range A.mulVecLin)
rw₆ :
  finrank R
      ↥(Submodule.map (↑(LinearEquiv.funCongrLeft R R em.symm) : (m → R) →ₗ[R] m₀ → R) (LinearMap.range A.mulVecLin)) =
    finrank R ↥(LinearMap.range A.mulVecLin)
rw₇ rw₈ : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
⊢ rank.{um₀, un₀, uR} (m := m₀) (n := n₀) (R := R) ((reindex em en : (a : Matrix m n R) → Matrix m₀ n₀ R) A) = A.rank

Tactic:
rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]

Premises used: Submodule.map_top, LinearMap.range_comp, Matrix.rank, Matrix.mulVecLin_reindex, LinearEquiv.finrank_map_eq, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Fintype n₀
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ rank.{um₀, un₀, uR} (m := m₀) (n := n₀) (A.submatrix (⇑em : (a : m₀) → m) (⇑en : (a : n₀) → n)) = A.rank

Tactic:
simpa only [reindex_apply] using rank_reindex em.symm en.symm A

Premises used: Matrix.reindex_apply, Matrix.rank_reindex, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
inst : CommRing R
n : Type un
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ lift.{um₀, max uR um} A.cRank ≤
    lift.{um, max uR um₀}
      (cRank.{um₀, un₀, uR} (m := m₀) (n := n₀) (A.submatrix (⇑em : (a : m₀) → m) (⇑en : (a : n₀) → n)))

Tactic:
simpa using ((A.reindex em.symm en.symm).lift_cRank_submatrix_le em.symm en.symm)

Premises used: Matrix.lift_cRank_submatrix_le, Matrix.reindex, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n₀ : Type un₀
R : Type uR
inst : CommRing R
m₀ : Type um
n : Type un
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ cRank.{um, un₀, uR} (m := m₀) (n := n₀) (A.submatrix (⇑em : (a : m₀) → m) (⇑en : (a : n₀) → n)) = A.cRank

Tactic:
simpa [-lift_cRank_submatrix] using A.lift_cRank_submatrix em en

Premises used: Matrix.lift_cRank_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
inst : CommRing R
n : Type un
A : Matrix m n R
em : m ≃ m₀
en : n ≃ n₀
⊢ lift.{um, max uR um₀}
      (cRank.{um₀, un₀, uR} (m := m₀) (n := n₀) (R := R) ((reindex em en : (a : Matrix m n R) → Matrix m₀ n₀ R) A)) =
    lift.{um₀, max uR um} A.cRank

Tactic:
lift_cRank_submatrix ..

Premises used: Matrix.submatrix, Matrix.lift_cRank_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n₀ : Type un₀
R : Type uR
inst : CommRing R
m₀ : Type um
n : Type un
A : Matrix m n R
em : m ≃ m₀
en : n ≃ n₀
⊢ cRank.{um, un₀, uR} (m := m₀) (n := n₀) (R := R) ((reindex em en : (a : Matrix m n R) → Matrix m₀ n₀ R) A) = A.cRank

Tactic:
cRank_submatrix ..

Premises used: Matrix.submatrix, Matrix.cRank_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
inst : CommRing R
n : Type un
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ eRank.{um₀, un₀, uR} (m := m₀) (n := n₀) (A.submatrix (⇑em : (a : m₀) → m) (⇑en : (a : n₀) → n)) = A.eRank

Tactic:
simpa [-lift_cRank_submatrix] using congr_arg Cardinal.toENat <| A.lift_cRank_submatrix em en

Premises used: Matrix.lift_cRank_submatrix, congr_arg, Cardinal.toENat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n₀ : Type un₀
R : Type uR
inst : CommRing R
m₀ : Type um
n : Type un
A : Matrix m n R
em : m ≃ m₀
en : n ≃ n₀
⊢ eRank.{um, un₀, uR} (m := m₀) (n := n₀) (R := R) ((reindex em en : (a : Matrix m n R) → Matrix m₀ n₀ R) A) = A.eRank

Tactic:
eRank_submatrix ..

Premises used: Matrix.submatrix, Matrix.eRank_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
intro :
  ∀ (val : Fintype m),
    A.rank =
      finrank.{uR, u_1} R
        ↥(LinearMap.range.{uR, uR, u_2, u_1} (R := R) (M := M₂) (τ₁₂ := RingHom.id R)
            ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A))
⊢ A.rank =
    finrank.{uR, u_1} R
      ↥(LinearMap.range.{uR, uR, u_2, u_1} (R := R) (M := M₂) (τ₁₂ := RingHom.id R)
          ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A))

Tactic:
cases nonempty_fintype m

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
⊢ A.rank =
    finrank.{uR, u_1} R
      ↥(LinearMap.range.{uR, uR, u_2, u_1} (R := R) (M := M₂) (τ₁₂ := RingHom.id R)
          ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A))

Tactic:
LinearEquiv.finrank_eq (e₁.ofSubmodules _ _ ?_)

Premises used: Matrix.rank, LinearEquiv.finrank_eq, LinearEquiv.ofSubmodules
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
intro :
  Submodule.map (↑e₁ : (m → R) →ₗ[R] M₁) (LinearMap.range A.mulVecLin) =
    LinearMap.range.{uR, uR, u_2, u_1} (R := R) (M := M₂) (τ₁₂ := RingHom.id R)
      ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A)
⊢ A.rank =
    finrank.{uR, u_1} R
      ↥(LinearMap.range.{uR, uR, u_2, u_1} (R := R) (M := M₂) (τ₁₂ := RingHom.id R)
          ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A))

Tactic:
refine LinearEquiv.finrank_eq (e₁.ofSubmodules _ _ ?_)

Premises used: LinearEquiv.finrank_eq, LinearEquiv.ofSubmodules
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
intro :
  ((↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin).range =
    LinearMap.range ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂))
⊢ Submodule.map (↑e₁ : (m → R) →ₗ[R] M₁) (LinearMap.range A.mulVecLin) =
    LinearMap.range.{uR, uR, u_2, u_1} (R := R) (M := M₂) (τ₁₂ := RingHom.id R)
      ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A)

Tactic:
rw [← LinearMap.range_comp, ← LinearMap.range_comp_of_range_eq_top (toLin v₂ v₁ A) e₂.range]

Premises used: LinearMap.range_comp_of_range_eq_top, Matrix.toLin, LinearMap.range_comp, DFunLike.coe, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
intro :
  (↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin =
    (toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂)
⊢ ((↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin).range =
    LinearMap.range ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂))

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
intro :
  ∀ (i : n),
    ((↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i =
      ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂)) ∘ₗ
        LinearMap.single R (fun (i : n) ↦ R) i
⊢ (↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin =
    (toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂)

Tactic:
apply LinearMap.pi_ext'

Premises used: LinearMap.pi_ext'
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
i : n
intro :
  Eq.{u_1 + 1} (α := M₁)
    ((((↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → M₁) 1 : M₁)
    ((((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂)) ∘ₗ
            LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → M₁)
        1 :
      M₁)
⊢ ((↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i =
    ((toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂)) ∘ₗ
      LinearMap.single R (fun (i : n) ↦ R) i

Tactic:
apply LinearMap.ext_ring

Premises used: LinearMap.ext_ring