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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₃ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
rw₄ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₅ : finrank R ↥(LinearMap.range A.mulVecLin) = A.rank
Tactic: rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₃ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
rw₄ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
rw₅ : finrank R ↥(LinearMap.range A.mulVecLin) = A.rank
⊢ Aᵀ.rank = A.rank
have rw₆ : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
Tactic: rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
⊢ Aᵀ.rank = A.rank
have rw : finrank R
    ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
        ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
            (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
          Aᵀ)) =
  A.rank
Tactic: classical
  rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₁ : finrank R
    ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
        ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
  A.rank
Tactic: classical
  rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₂ : finrank R
    ↥(LinearMap.range (M := Dual R (m → R))
        (LinearMap.dualMap
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
  A.rank
Tactic: classical
  rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₃ : finrank R
    ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
        ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
  A.rank
Tactic: classical
  rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₃ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₄ : finrank R
    ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
        ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
  A.rank
Tactic: classical
  rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₃ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
rw₄ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
⊢ Aᵀ.rank = A.rank
have rw₅ : finrank R ↥(LinearMap.range A.mulVecLin) = A.rank
Tactic: classical
  rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Fintype m
A : Matrix m n R
rw :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((toLin (Basis.dualBasis (Pi.basisFun R m)) (Basis.dualBasis (Pi.basisFun R n)) :
              (a : Matrix n m R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            Aᵀ)) =
    A.rank
rw₁ :
  finrank R
      ↥(LinearMap.range (R := R) (M := Dual R (m → R)) (τ₁₂ := RingHom.id R)
          ((Dual.transpose : (a : (n → R) →ₗ[R] m → R) → Dual R (m → R) →ₗ[R] Dual R (n → R))
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₂ :
  finrank R
      ↥(LinearMap.range (M := Dual R (m → R))
          (LinearMap.dualMap
            ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A))) =
    A.rank
rw₃ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin (Pi.basisFun R n) (Pi.basisFun R m) : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
rw₄ :
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A)) =
    A.rank
rw₅ : finrank R ↥(LinearMap.range A.mulVecLin) = A.rank
⊢ Aᵀ.rank = A.rank
have rw₆ : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
Tactic: classical
  rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
      toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
      toLin_eq_toLin', toLin'_apply', rank]
-- 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 : Field R
inst_2 : Finite m
A : Matrix m n R
⊢ A.rank = finrank R ↥(span R (range A.row))
have intro : ∀ (val : Fintype m), A.rank = finrank R ↥(span R (range A.row))
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 : Field R
inst_2 : Finite m
A : Matrix m n R
val : Fintype m
⊢ A.rank = finrank R ↥(span R (range A.row))
have intro : Aᵀ.rank = finrank R ↥(span R (range A.row))
Tactic: rw [← rank_transpose, rank_eq_finrank_span_cols, col_transpose]
-- 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 : Field R
inst_2 : Finite m
A : Matrix m n R
val : Fintype m
intro : Aᵀ.rank = finrank R ↥(span R (range A.row))
⊢ A.rank = finrank R ↥(span R (range A.row))
have intro₁ : finrank R ↥(span R (range Aᵀ.col)) = finrank R ↥(span R (range A.row))
Tactic: rw [← rank_transpose, rank_eq_finrank_span_cols, col_transpose]
-- 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 : Field R
inst_2 : Finite m
A : Matrix m n R
val : Fintype m
intro : Aᵀ.rank = finrank R ↥(span R (range A.row))
intro₁ : finrank R ↥(span R (range Aᵀ.col)) = finrank R ↥(span R (range A.row))
⊢ A.rank = finrank R ↥(span R (range A.row))
have intro₂ : finrank R ↥(span R (range A.row)) = finrank R ↥(span R (range A.row))
Tactic: rw [← rank_transpose, rank_eq_finrank_span_cols, col_transpose]
-- 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 : Field R
inst_2 : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
⊢ M.rank = Fintype.card m
have rw : finrank R ↥(span R (range M.row)) = Fintype.card m
Tactic: rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]
-- 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 : Field R
inst_2 : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
rw : finrank R ↥(span R (range M.row)) = Fintype.card m
⊢ M.rank = Fintype.card m
have rw₁ : finrank R ↥(span R (range M.row)) = Set.finrank R (range M.row)
Tactic: rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]
-- 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 : Field R
inst_2 : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
rw : finrank R ↥(span R (range M.row)) = Fintype.card m
rw₁ : finrank R ↥(span R (range M.row)) = Set.finrank R (range M.row)
⊢ M.rank = Fintype.card m
have rw₂ : finrank R ↥(span R (range M.row)) = finrank R ↥(span R (range M.row))
Tactic: rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Finite l
inst_3 : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B)) ≤
    finrank R
      ↥(LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
          ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
have hst : LE.le (α := Submodule R (m → R))
  (LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
    ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B))
  (LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
    ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
Tactic: apply Submodule.finrank_mono
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Finite l
inst_3 : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ LE.le (α := Submodule R (m → R))
    (LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
      ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B))
    (LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
      ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
have hst : Eq (α := (n → R) →ₗ[R] l → R)
  ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A ∘ₗ
    (toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B)
  0
Tactic: rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Finite l
inst_3 : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
hst :
  Eq (α := (n → R) →ₗ[R] l → R)
    ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A ∘ₗ
      (toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B)
    0
⊢ LE.le (α := Submodule R (m → R))
    (LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
      ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B))
    (LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
      ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
have hst₁ : Eq (α := (n → R) →ₗ[R] l → R) ((toLin en el : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) (A * B) : (n → R) →ₗ[R] l → R)
  (0 : (n → R) →ₗ[R] l → R)
Tactic: rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Finite l
inst_3 : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
hst :
  Eq (α := (n → R) →ₗ[R] l → R)
    ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A ∘ₗ
      (toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B)
    0
hst₁ :
  Eq (α := (n → R) →ₗ[R] l → R) ((toLin en el : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) (A * B) : (n → R) →ₗ[R] l → R)
    (0 : (n → R) →ₗ[R] l → R)
⊢ LE.le (α := Submodule R (m → R))
    (LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
      ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B))
    (LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
      ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
have hst₂ : Eq (α := (n → R) →ₗ[R] l → R) ((toLin en el : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) 0) 0
Tactic: rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Finite l
inst_3 : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
hst :
  Eq (α := (n → R) →ₗ[R] l → R)
    ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A ∘ₗ
      (toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B)
    0
hst₁ :
  Eq (α := (n → R) →ₗ[R] l → R) ((toLin en el : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) (A * B) : (n → R) →ₗ[R] l → R)
    (0 : (n → R) →ₗ[R] l → R)
hst₂ : Eq (α := (n → R) →ₗ[R] l → R) ((toLin en el : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) 0) 0
⊢ LE.le (α := Submodule R (m → R))
    (LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
      ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B))
    (LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
      ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
have hst₃ : Eq (α := (n → R) →ₗ[R] l → R) 0 0
Tactic: rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Finite l
inst_3 : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
let let₁ let₂ let₃ let₄ : A.rank + B.rank ≤ Fintype.card m
⊢ A.rank + B.rank ≤ Fintype.card m
have let₅ : let el : Basis l R (l → R) := Pi.basisFun R l;
let em : Basis m R (m → R) := Pi.basisFun R m;
let en : Basis n R (n → R) := Pi.basisFun R n;
finrank R
    ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
        ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B)) ≤
  finrank R
    ↥(LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
        ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
Tactic: classical
  let el : Basis l R (l → R) := Pi.basisFun R l
  let em : Basis m R (m → R) := Pi.basisFun R m
  let en : Basis n R (n → R) := Pi.basisFun R n
  rw [Matrix.rank_eq_finrank_range_toLin A el em,
      Matrix.rank_eq_finrank_range_toLin B em en,
      ← Module.finrank_fintype_fun_eq_card R,
      ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
      add_le_add_iff_left]
  apply Submodule.finrank_mono
  rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]