awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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))
⊢ (A * B).rank = B.rank
have hAB : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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
⊢ (A.submatrix r c).rank ≤ A.rank
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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
⊢ (A.submatrix r c).rank ≤ A.rank
have this : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)ᵀᵀ.submatrix id c)ᵀᵀ.rank ≤ finrank R ↥(span R (range (A.submatrix r id).col))
have rw : finrank R ↥(span R (range ((A.submatrix r id).submatrix id c).col)) ≤ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)) = (A.submatrix r id)ᵀᵀ.rank
have rw : finrank R ↥(span R (range (A.submatrix r id).col)) = finrank R ↥(span R (range (A.submatrix r id)ᵀ.row))
Tactic: rw [rank, Matrix.mulVecLin_transpose, range_vecMulLinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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.rank
have calc : rank (n := n) (A.submatrix r (⇑(Equiv.refl n) : (a : n) → n)) ≤ 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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))
⊢ rank (n := n) (A.submatrix r (⇑(Equiv.refl n) : (a : n) → n)) ≤ A.rank
have calc : finrank R ↥(Submodule.map (LinearMap.funLeft R R r) (LinearMap.range A.mulVecLin)) ≤
  finrank R ↥(LinearMap.range A.mulVecLin)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ 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
have rw : finrank R ↥(LinearMap.range (M := n₀ → R) (mulVecLin ((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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ 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
have 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)
Tactic: rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ 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
have 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)
Tactic: rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ 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
have 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)
Tactic: rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ 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
have 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)
Tactic: rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ 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
have 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)
Tactic: rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ 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
have 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)
Tactic: rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ 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
have rw₇ : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
Tactic: rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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₂
⊢ 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))
have 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))
Tactic: cases nonempty_fintype m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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))
have 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)
Tactic: refine LinearEquiv.finrank_eq (e₁.ofSubmodules _ _ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ 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)
have 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₂))
Tactic: rw [← LinearMap.range_comp, ← LinearMap.range_comp_of_range_eq_top (toLin v₂ v₁ A) e₂.range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ ((↑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₂))
have 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₂)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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)
⊢ (↑e₁ : (m → R) →ₗ[R] M₁) ∘ₗ A.mulVecLin =
    (toLin v₂ v₁ : (a : Matrix m n R) → M₂ →ₗ[R] M₁) A ∘ₗ (↑e₂ : (n → R) →ₗ[R] M₂)
have 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
Tactic: apply LinearMap.pi_ext'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ ((↑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
have 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₁)
Tactic: apply LinearMap.ext_ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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
⊢ 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₁)
have aux₁ : Eq (α := m → R)
  ((((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A : (n → R) →ₗ[R] m → R) :
        (a : n → R) → m → R)
      ((Pi.basisFun R n : (a : n) → n → R) i : n → R) :
    m → R)
  (∑ j : m, HSMul.hSMul (β := m → R) (A j i) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : m → R)
Tactic: have aux₁ := toLin_self (Pi.basisFun R n) (Pi.basisFun R m) A i