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 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker (Aᴴ * A).mulVecLin) x ↔
    Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker A.mulVecLin) x

Tactic:
simp only [LinearMap.mem_ker, mulVecLin_apply, conjTranspose_mul_self_mulVec_eq_zero]

Premises used: Matrix.conjTranspose_mul_self_mulVec_eq_zero, Matrix.mulVecLin_apply, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) ?_

Premises used: LinearMap.ker, Membership.mem, Subtype, Matrix.mulVecLin, add_left_injective, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
refine :
  Eq (α := ℕ)
    ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin)))
    ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin)))
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
refine add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) ?_

Premises used: LinearMap.ker, Membership.mem, Subtype, Matrix.mulVecLin, add_left_injective, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
trans :
  finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin)
trans₁ :
  finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Tactic:
trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) }

Premises used: HMul.hMul, LinearMap.ker, Membership.mem, LinearMap.range, Subtype, Matrix.mulVecLin, Matrix.conjTranspose, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
rw rw₁ :
  finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin)

Tactic:
rw [ker_mulVecLin_conjTranspose_mul_self]

Premises used: Matrix.ker_mulVecLin_conjTranspose_mul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᴴ * A).mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Tactic:
simp only [LinearMap.finrank_range_add_finrank_ker]

Premises used: LinearMap.finrank_range_add_finrank_ker
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ Aᴴ.rank = A.rank

Tactic:
le_antisymm
    (((rank_conjTranspose_mul_self _).symm.trans_le <| rank_mul_le_left _ _).trans_eq <|
      congr_arg _ <| conjTranspose_conjTranspose _)
    ((rank_conjTranspose_mul_self _).symm.trans_le <| rank_mul_le_left _ _)

Premises used: LE.le.trans_eq, Eq.trans_le, congr_arg, le_antisymm, Matrix.rank_mul_le_left, Eq.symm, Matrix.conjTranspose_conjTranspose, Matrix.rank_conjTranspose_mul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : PartialOrder R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).rank = A.rank

Tactic:
simpa only [rank_conjTranspose, conjTranspose_conjTranspose] using
    rank_conjTranspose_mul_self Aᴴ

Premises used: Matrix.rank_conjTranspose, Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose, Matrix.rank_conjTranspose_mul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
h :
  ∀ (x : n → R),
    Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker (Aᵀ * A).mulVecLin) x ↔
      Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker A.mulVecLin) x
⊢ Eq (α := Submodule R (n → R)) (LinearMap.ker (Aᵀ * A).mulVecLin) (LinearMap.ker A.mulVecLin)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
⊢ Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker (Aᵀ * A).mulVecLin) x ↔
    Membership.mem (γ := Submodule R (n → R)) (LinearMap.ker A.mulVecLin) x

Tactic:
simp only [LinearMap.mem_ker, mulVecLin_apply, ← mulVec_mulVec]

Premises used: Matrix.mulVecLin_apply, LinearMap.mem_ker, Matrix.mulVec_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : Aᵀ *ᵥ A *ᵥ x = 0 → A *ᵥ x = 0
h₁ : A *ᵥ x = 0 → Aᵀ *ᵥ A *ᵥ x = 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : Aᵀ *ᵥ A *ᵥ x = 0
⊢ x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0

Tactic:
replace h := congr_arg (dotProduct x) h
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ Aᵀ *ᵥ A *ᵥ x = x ⬝ᵥ 0
h₁ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = x ⬝ᵥ 0), A *ᵥ x = 0
h₂ : ∀ (h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
h₃ : ∀ (h : A *ᵥ x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
h₄ h₅ h₆ h₇ : ∀ (h : A *ᵥ x = 0), A *ᵥ x = 0
⊢ A *ᵥ x = 0

Tactic:
rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h

Premises used: dotProduct_self_eq_zero, dotProduct_zero, Matrix.vecMul_transpose, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : A *ᵥ x = 0
h₁ : Aᵀ *ᵥ 0 = 0
h₂ h₃ : Eq (α := n → R) 0 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0

Tactic:
rw [h, mulVec_zero]

Premises used: Matrix.mulVec_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
add_left_injective (finrank R <| LinearMap.ker A.mulVecLin) ?_

Premises used: LinearMap.ker, Membership.mem, Subtype, Matrix.mulVecLin, add_left_injective, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
refine :
  Eq (α := ℕ)
    ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin)))
    ((fun (x : ℕ) ↦ x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin)))
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
refine add_left_injective (finrank R <| LinearMap.ker A.mulVecLin) ?_

Premises used: LinearMap.ker, Membership.mem, Subtype, Matrix.mulVecLin, add_left_injective, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
trans :
  finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin)
trans₁ :
  finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Tactic:
trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }

Premises used: HMul.hMul, LinearMap.ker, Membership.mem, LinearMap.range, Subtype, Matrix.mulVecLin, Matrix.transpose, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
rw rw₁ :
  finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin)

Tactic:
rw [ker_mulVecLin_transpose_mul_self]

Premises used: Matrix.ker_mulVecLin_transpose_mul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Fintype m
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Tactic:
simp only [LinearMap.finrank_range_add_finrank_ker]

Premises used: LinearMap.finrank_range_add_finrank_ker
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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
rw₆ rw₇ : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
⊢ Aᵀ.rank = 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]

Premises used: Matrix.rank, Matrix.rank_eq_finrank_range_toLin, Matrix.toLin'_apply', Module.Basis.dualBasis, LinearMap.finrank_range_dualMap_eq_finrank_range, Matrix.transpose, LinearMap.dualMap_def, Matrix.toLin_transpose, Matrix.toLin_eq_toLin', Pi.basisFun
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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
rw₆ rw₇ : finrank R ↥(LinearMap.range A.mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
⊢ Aᵀ.rank = 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]

Premises used: Matrix.rank, Matrix.toLin'_apply', LinearMap.finrank_range_dualMap_eq_finrank_range, LinearMap.dualMap_def, Matrix.toLin_transpose, Matrix.toLin_eq_toLin'
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : Fintype m
A : Matrix m n R
⊢ (A * Aᵀ).rank = A.rank

Tactic:
simpa only [rank_transpose, transpose_transpose] using rank_transpose_mul_self Aᵀ

Premises used: Matrix.rank_transpose, Matrix.transpose_transpose, Matrix.rank_transpose_mul_self, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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
intro : ∀ (val : Fintype m), A.rank = finrank R ↥(span R (range A.row))
⊢ A.rank = finrank R ↥(span R (range A.row))

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 : 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))
intro₂ intro₃ : finrank R ↥(span R (range A.row)) = finrank R ↥(span R (range A.row))
⊢ A.rank = finrank R ↥(span R (range A.row))

Tactic:
rw [← rank_transpose, rank_eq_finrank_span_cols, col_transpose]

Premises used: Matrix.rank_transpose, Matrix.col_transpose, Matrix.rank_eq_finrank_span_cols
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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)
rw₂ rw₃ : finrank R ↥(span R (range M.row)) = finrank R ↥(span R (range M.row))
⊢ M.rank = Fintype.card m

Tactic:
rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]

Premises used: Set.finrank, Matrix.rank_eq_finrank_span_row, Iff.mp, linearIndependent_iff_card_eq_finrank_span
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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 :
  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))
⊢ 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:
apply Submodule.finrank_mono

Premises used: Submodule.finrank_mono
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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
hst₃ hst₄ : Eq (α := (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))

Tactic:
rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]

Premises used: map_zero, Matrix.toLin_mul, LinearMap.range_le_ker_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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
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))
hst :
  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;
  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))
⊢ A.rank + B.rank ≤ Fintype.card m

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]

Premises used: add_le_add_iff_left, map_zero, Matrix.toLin_mul, Submodule.finrank_mono, Module.finrank_fintype_fun_eq_card, LinearMap.range_le_ker_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
⊢ Nontrivial K

Tactic:
nontriviality K
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
h : Nontrivial K
rw :
  LinearMap.rank (V := n → K) (V' := m → K)
      ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w) ∘ₗ
        (toLin' : (a : Matrix (Fin 1) n K) → (n → K) →ₗ[K] Fin 1 → K) (replicateRow (Fin 1) v)) ≤
    1
⊢ LinearMap.rank (K := K) (V := n → K) (V' := m → K)
      ((toLin' : (a : Matrix m n K) → (n → K) →ₗ[K] m → K) (vecMulVec w v)) ≤
    1

Tactic:
rw [Matrix.vecMulVec_eq (Fin 1), Matrix.toLin'_mul]

Premises used: Matrix.toLin'_mul, Matrix.vecMulVec_eq, OfNat.ofNat, Fin
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
h : Nontrivial K
⊢ LinearMap.rank (V := n → K) (V' := m → K)
      ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w) ∘ₗ
        (toLin' : (a : Matrix (Fin 1) n K) → (n → K) →ₗ[K] Fin 1 → K) (replicateRow (Fin 1) v)) ≤
    1

Tactic:
le_trans (LinearMap.rank_comp_le_left _ _) ?_

Premises used: LinearMap.rank_comp_le_left, le_trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
h : Nontrivial K
refine :
  LinearMap.rank (K := K) (V := Fin 1 → K) (V' := m → K)
      ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w)) ≤
    1
⊢ LinearMap.rank (V := n → K) (V' := m → K)
      ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w) ∘ₗ
        (toLin' : (a : Matrix (Fin 1) n K) → (n → K) →ₗ[K] Fin 1 → K) (replicateRow (Fin 1) v)) ≤
    1

Tactic:
refine le_trans (LinearMap.rank_comp_le_left _ _) ?_

Premises used: LinearMap.rank_comp_le_left, le_trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
h : Nontrivial K
⊢ LinearMap.rank (K := K) (V := Fin 1 → K) (V' := m → K)
      ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w)) ≤
    1

Tactic:
(LinearMap.rank_le_domain _).trans_eq ?_

Premises used: LinearMap.rank_le_domain, LE.le.trans_eq