awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).eRank ≤ A.eRank

Tactic:
simpa using OrderHom.mono (β := ℕ∞) Cardinal.toENat <| lift_cRank_submatrix_le A r c

Premises used: Matrix.lift_cRank_submatrix_le, OrderHom.mono
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
inr :
  ∀
    (this :
      ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
        (hfin : Finite n), A.eRank ≤ ENat.card n)
    (hfin : ¬Finite n), A.eRank ≤ ENat.card n
wlog :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite n), A.eRank ≤ ENat.card n
⊢ A.eRank ≤ ENat.card n

Tactic:
wlog hfin : Finite n

Premises used: Finite
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite n), A.eRank ≤ ENat.card n
hfin : ¬Finite n
⊢ Infinite n

Tactic:
simpa using hfin
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite n), A.eRank ≤ ENat.card n
hfin : ¬Finite n
⊢ A.eRank ≤ ENat.card n

Tactic:
simp [ENat.card_eq_top.2 (by simpa using hfin)]

Premises used: Iff.mpr, ENat.card_eq_top
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite n
have : ∀ (x : Fintype n), A.eRank ≤ ENat.card n
⊢ A.eRank ≤ ENat.card n

Tactic:
have _ := Fintype.ofFinite n
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite n
x : Fintype n
rw : A.cRank ≤ (↑(Fintype.card n) : Cardinal.{max uR um})
⊢ A.eRank ≤ ENat.card n

Tactic:
rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_natCast]

Premises used: Matrix.eRank, Cardinal.toENat_le_natCast, ENat.card_eq_coe_fintype_card
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite n
x : Fintype n
⊢ A.cRank ≤ (↑(Fintype.card n) : Cardinal.{max uR um})

Tactic:
A.cRank_le_card_width

Premises used: Matrix.cRank_le_card_width
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite n
x : Fintype n
⊢ A.cRank ≤ (↑(Fintype.card n) : Cardinal.{max uR um})

Tactic:
exact A.cRank_le_card_width

Premises used: Matrix.cRank_le_card_width
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
inr :
  ∀
    (this :
      ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
        (hfin : Finite m), A.eRank ≤ ENat.card m)
    (hfin : ¬Finite m), A.eRank ≤ ENat.card m
wlog :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite m), A.eRank ≤ ENat.card m
⊢ A.eRank ≤ ENat.card m

Tactic:
wlog hfin : Finite m

Premises used: Finite
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite m), A.eRank ≤ ENat.card m
hfin : ¬Finite m
⊢ Infinite m

Tactic:
simpa using hfin
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite m), A.eRank ≤ ENat.card m
hfin : ¬Finite m
⊢ A.eRank ≤ ENat.card m

Tactic:
simp [ENat.card_eq_top.2 (by simpa using hfin)]

Premises used: Iff.mpr, ENat.card_eq_top
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite m
have : ∀ (x : Fintype m), A.eRank ≤ ENat.card m
⊢ A.eRank ≤ ENat.card m

Tactic:
have _ := Fintype.ofFinite m
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite m
x : Fintype m
rw : A.cRank ≤ (↑(Fintype.card m) : Cardinal.{max uR um})
⊢ A.eRank ≤ ENat.card m

Tactic:
rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_natCast]

Premises used: Matrix.eRank, Cardinal.toENat_le_natCast, ENat.card_eq_coe_fintype_card
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite m
x : Fintype m
⊢ A.cRank ≤ (↑(Fintype.card m) : Cardinal.{max uR um})

Tactic:
A.cRank_le_card_height

Premises used: Matrix.cRank_le_card_height
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m_1 : Type um
n_1 : Type un
R_1 : Type uR
inst : Semiring R_1
m : Type um
n : Type un
R : Type uR
inst_1 : Semiring R
inst_2 : StrongRankCondition R
A : Matrix m n R
hfin : Finite m
x : Fintype m
⊢ A.cRank ≤ (↑(Fintype.card m) : Cardinal.{max uR um})

Tactic:
exact A.cRank_le_card_height

Premises used: Matrix.cRank_le_card_height
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
inr :
  ∀
    (this :
      ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
        (hfin : Finite m), A.eRank ≤ ENat.card m)
    (hfin : ¬Finite m), A.eRank ≤ ENat.card m
wlog wlog₁ :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite m), A.eRank ≤ ENat.card m
wlog₂ :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite m) (x : Fintype m), A.eRank ≤ ENat.card m
wlog₃ :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R)
    (hfin : Finite m) (x : Fintype m), A.cRank ≤ (↑(Fintype.card m) : Cardinal.{max uR um})
⊢ A.eRank ≤ ENat.card m

Tactic:
classical
  wlog hfin : Finite m
  · simp [ENat.card_eq_top.2 (by simpa using hfin)]
  have _ := Fintype.ofFinite m
  rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_natCast]
  exact A.cRank_le_card_height

Premises used: Iff.mpr, Matrix.eRank, Finite, ENat.card_eq_top, Cardinal.toENat_le_natCast, ENat.card_eq_coe_fintype_card
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Subsingleton R
A : Matrix m n R
⊢ A.rank = 1

Tactic:
finrank_subsingleton

Premises used: Matrix.rank, Module.finrank_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
⊢ LinearIndependent R (M := (j : m) → R) fun (i : m) ↦ Pi.single (M := fun (i : m) ↦ R) i 1

Tactic:
Pi.linearIndependent_single_one m R

Premises used: Pi.linearIndependent_single_one
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
h : ∀ (x : m), Eq (α := m → R) (1ᵀ x) (Pi.single (M := fun (i : m) ↦ R) x 1)
⊢ LinearIndependent (ι := m) R (M := m → R) 1ᵀ

Tactic:
convert! Pi.linearIndependent_single_one m R

Premises used: Pi.linearIndependent_single_one
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
x : m
⊢ Eq (α := m → R) (1ᵀ x) (Pi.single (M := fun (i : m) ↦ R) x 1)

Tactic:
simp [funext_iff, Matrix.one_eq_pi_single]

Premises used: Matrix.one_eq_pi_single, funext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
⊢ LinearIndependent (ι := m) R (M := m → R) 1ᵀ

Tactic:
have h : LinearIndependent R (1 : Matrix m m R)ᵀ := by
    convert! Pi.linearIndependent_single_one m R
    simp [funext_iff, Matrix.one_eq_pi_single]
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
h : LinearIndependent (ι := m) R (M := m → R) 1ᵀ
rw : Module.rank R ↥(span R (range (ι := m) 1ᵀ)) = lift.{uR, um} #m
rw₁ : #(↑(range (ι := m) 1ᵀ) : Type (max uR um)) = lift.{uR, um} #m
rw₂ : #(↑(range (ι := m) 1ᵀ) : Type (max uR um)) = lift.{max um uR, um} #m
rw₃ : #(↑(range (ι := m) 1ᵀ) : Type (max uR um)) = lift.{um, max uR um} #(↑(range (ι := m) 1ᵀ) : Type (max uR um))
rw₄ rw₅ : #(↑(range (ι := m) 1ᵀ) : Type (max uR um)) = #(↑(range (ι := m) 1ᵀ) : Type (max uR um))
⊢ cRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = lift.{uR, um} #m

Tactic:
rw [cRank, rank_span h, ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']

Premises used: Cardinal.mk_range_eq_of_injective, Cardinal.lift_id', LinearIndependent.injective, Matrix.cRank, Cardinal.lift_umax, rank_span
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
rw : (toENat : (a : Cardinal.{max uR um}) → ℕ∞) (cRank.{um, um, uR} (m := m) (n := m) (R := R) 1) = ENat.card m
rw₁ : (toENat : (a : Cardinal.{max uR um}) → ℕ∞) (lift.{uR, um} #m) = ENat.card m
rw₂ : (toENat : (a : Cardinal.{um}) → ℕ∞) #m = ENat.card m
rw₃ rw₄ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{um}) → ℕ∞) #m : ℕ∞) ((toENat : (a : Cardinal.{um}) → ℕ∞) #m : ℕ∞)
⊢ eRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = ENat.card m

Tactic:
rw [eRank, cRank_one, toENat_lift, ENat.card]

Premises used: Matrix.eRank, Cardinal.toENat_lift, Matrix.cRank_one, ENat.card
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
rw : finrank R ↥(LinearMap.range (M := n → R) (mulVecLin 1)) = Fintype.card n
rw₁ : finrank R ↥(LinearMap.range LinearMap.id) = Fintype.card n
rw₂ : finrank R ↥⊤ = Fintype.card n
rw₃ : finrank R (n → R) = Fintype.card n
rw₄ rw₅ : Fintype.card n = Fintype.card n
⊢ rank.{un, un, uR} (m := n) (n := n) (R := R) 1 = Fintype.card n

Tactic:
rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]

Premises used: LinearMap.range_id, Matrix.rank, Matrix.mulVecLin_one, Module.finrank_pi, finrank_top
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
rw : finrank R ↥(LinearMap.range (M := n → R) (mulVecLin 0)) = 0
rw₁ : finrank R ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R) 0) = 0
rw₂ : finrank R ↥⊥ = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ rank.{um, un, uR} (m := m) (n := n) (R := R) 0 = 0

Tactic:
rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]

Premises used: LinearMap.range_zero, Matrix.mulVecLin_zero, Matrix.rank, finrank_bot
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
R : Type uR
inst : CommRing R
m : Type u_1
n : Type u_2
inst_1 : Nontrivial R
inl : ∀ (hn : IsEmpty n), cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
inr : ∀ (hn : Nonempty n), cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0

Tactic:
obtain hn | hn := isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
R : Type uR
inst : CommRing R
m : Type u_1
n : Type u_2
inst_1 : Nontrivial R
hn : IsEmpty n
inl : Module.rank R ↥(span R (range (ι := n) 0ᵀ)) = 0
inl₁ : Module.rank R ↥(span R ∅) = 0
inl₂ : Module.rank R ↥⊥ = 0
inl₃ inl₄ : Eq (α := Cardinal.{max uR u_1}) 0 0
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0

Tactic:
rw [cRank, range_eq_empty, span_empty, rank_bot]

Premises used: rank_bot, Matrix.cRank, Submodule.span_empty, Set.range_eq_empty
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
R : Type uR
inst : CommRing R
m : Type u_1
n : Type u_2
inst_1 : Nontrivial R
hn : Nonempty n
inr : Module.rank R ↥(span R (range (ι := n) 0ᵀ)) = 0
inr₁ : Module.rank R ↥(span R (range (ι := n) 0)) = 0
inr₂ : Module.rank R ↥(R ∙ 0) = 0
inr₃ : Module.rank R ↥⊥ = 0
inr₄ inr₅ : Eq (α := Cardinal.{max uR u_1}) 0 0
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0

Tactic:
rw [cRank, transpose_zero, range_zero, span_zero_singleton, rank_bot]

Premises used: rank_bot, Set.range_zero, Matrix.transpose_zero, Matrix.cRank, Submodule.span_zero_singleton
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
R : Type uR
inst : CommRing R
m : Type u_1
n : Type u_2
inst_1 : Nontrivial R
⊢ eRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0

Tactic:
simp [eRank]

Premises used: Matrix.eRank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
A : Matrix m n R
⊢ A.rank ≤ Fintype.card n

Tactic:
A.mulVecLin.finrank_range_le.trans_eq (finrank_pi _)

Premises used: LE.le.trans_eq, Set.Mem, Matrix.rank, Module.finrank_pi, LinearMap.finrank_range_le, Matrix.mulVecLin
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
A : Matrix m n R
⊢ A.rank ≤ Fintype.card n

Tactic:
exact A.mulVecLin.finrank_range_le.trans_eq (finrank_pi _)

Premises used: LE.le.trans_eq, Module.finrank_pi, LinearMap.finrank_range_le, Matrix.mulVecLin
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
m n : ℕ
A : Matrix (Fin m) (Fin n) R
⊢ A.rank ≤ n

Tactic:
A.rank_le_card_width.trans <| (Fintype.card_fin n).le

Premises used: Fintype.card_fin, Eq.le, Matrix.rank_le_card_width, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
h : Nontrivial R
rw : finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range A.mulVecLin)
⊢ (A * B).rank ≤ A.rank

Tactic:
rw [rank, rank, mulVecLin_mul]

Premises used: Matrix.rank, Matrix.mulVecLin_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
h : Nontrivial R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
Cardinal.toNat_le_toNat (LinearMap.rank_comp_le_left _ _) (rank_lt_aleph0 _ _)

Premises used: LinearMap.rank_comp_le_left, Cardinal.toNat_le_toNat, Module.rank_lt_aleph0, Module.finrank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
h : Nontrivial R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
exact Cardinal.toNat_le_toNat (LinearMap.rank_comp_le_left _ _) (rank_lt_aleph0 _ _)

Premises used: LinearMap.rank_comp_le_left, Cardinal.toNat_le_toNat, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
h : Nontrivial R
rw : finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range B.mulVecLin)
⊢ (A * B).rank ≤ B.rank

Tactic:
rw [rank, rank, mulVecLin_mul]

Premises used: Matrix.rank, Matrix.mulVecLin_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
h : Nontrivial R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range B.mulVecLin)

Tactic:
finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _)
    (rank_lt_aleph0 _ _)

Premises used: LinearMap.lift_rank_comp_le_right, Module.finrank_le_finrank_of_rank_le_rank, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
h : Nontrivial R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range B.mulVecLin)

Tactic:
exact finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _)
    (rank_lt_aleph0 _ _)

Premises used: LinearMap.lift_rank_comp_le_right, Module.finrank_le_finrank_of_rank_le_rank, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommRing R
A : Matrix m n R
B : Matrix n o R
⊢ (A * B).rank ≤ min A.rank B.rank

Tactic:
le_min (rank_mul_le_left _ _) (rank_mul_le_right _ _)

Premises used: Matrix.rank_mul_le_right, le_min, Matrix.rank_mul_le_left
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
w : m → R
v : n → R
rw : (replicateCol Unit w * replicateRow Unit v).rank ≤ 1
⊢ (vecMulVec w v).rank ≤ 1

Tactic:
rw [Matrix.vecMulVec_eq Unit]

Premises used: Matrix.vecMulVec_eq, Unit
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
w : m → R
v : n → R
⊢ (replicateCol Unit w * replicateRow Unit v).rank ≤ 1

Tactic:
le_trans (rank_mul_le_left _ _) ?_

Premises used: Matrix.rank_mul_le_left, le_trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
w : m → R
v : n → R
refine : (replicateCol Unit w).rank ≤ 1
⊢ (replicateCol Unit w * replicateRow Unit v).rank ≤ 1

Tactic:
refine le_trans (rank_mul_le_left _ _) ?_

Premises used: Matrix.rank_mul_le_left, le_trans
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
w : m → R
v : n → R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
w : m → R
v : n → R
h : Nontrivial R
⊢ (replicateCol Unit w).rank ≤ 1

Tactic:
rank_le_card_width _

Premises used: Fintype.card, Matrix.rank_le_card_width, Finset.card, Multiset.card
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
w : m → R
v : n → R
h : Nontrivial R
⊢ (replicateCol Unit w).rank ≤ 1

Tactic:
exact rank_le_card_width _

Premises used: Matrix.rank_le_card_width
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
A : (Matrix n n R)ˣ
apply : Fintype.card n ≤ (↑A : Matrix n n R).rank
⊢ (↑A : Matrix n n R).rank = Fintype.card n

Tactic:
apply le_antisymm (rank_le_card_width (A : Matrix n n R)) _

Premises used: Units.val, Matrix.rank_le_card_width, le_antisymm
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
A : (Matrix n n R)ˣ
⊢ ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)).rank ≤ (↑A : Matrix n n R).rank

Tactic:
have := rank_mul_le_left (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
A : (Matrix n n R)ˣ
this : ((↑A : Matrix n n R) * (↑A⁻¹ : Matrix n n R)).rank ≤ (↑A : Matrix n n R).rank
rwa : ∀ (this : (↑(A * A⁻¹) : Matrix n n R).rank ≤ (↑A : Matrix n n R).rank), Fintype.card n ≤ (↑A : Matrix n n R).rank
rwa₁ :
  ∀ (this : rank.{un, un, uR} (m := n) (n := n) (R := R) (↑1 : Matrix n n R) ≤ (↑A : Matrix n n R).rank),
    Fintype.card n ≤ (↑A : Matrix n n R).rank
rwa₂ :
  ∀ (this : rank.{un, un, uR} (m := n) (n := n) (R := R) 1 ≤ (↑A : Matrix n n R).rank),
    Fintype.card n ≤ (↑A : Matrix n n R).rank
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : Fintype.card n ≤ (↑A : Matrix n n R).rank), Fintype.card n ≤ (↑A : Matrix n n R).rank
⊢ Fintype.card n ≤ (↑A : Matrix n n R).rank

Tactic:
rwa [← Units.val_mul, mul_inv_cancel, Units.val_one, rank_one] at this

Premises used: Matrix.rank_one, Units.val_one, mul_inv_cancel, Units.val_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
A : Matrix n n R
h : IsUnit A
obtain : ∀ (A : (Matrix n n R)ˣ), (↑A : Matrix n n R).rank = Fintype.card n
⊢ A.rank = Fintype.card n

Tactic:
obtain ⟨A, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
A : (Matrix n n R)ˣ
⊢ (↑A : Matrix n n R).rank = Fintype.card n

Tactic:
rank_unit A

Premises used: Matrix.rank_unit
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
A : (Matrix n n R)ˣ
⊢ (↑A : Matrix n n R).rank = Fintype.card n

Tactic:
exact rank_unit A

Premises used: Matrix.rank_unit
-- 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
this : Function.Surjective (α := n → R) (β := n → R) (⇑A.mulVecLin : (a : n → R) → n → R)
rw : finrank R ↥(LinearMap.range (B * A).mulVecLin) = B.rank
rw₁ : finrank R ↥(B.mulVecLin ∘ₗ A.mulVecLin).range = B.rank
rw₂ : finrank R ↥(LinearMap.range B.mulVecLin) = B.rank
rw₃ rw₄ : B.rank = B.rank
⊢ (B * A).rank = B.rank

Tactic:
rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
      (LinearMap.range_eq_top.mpr this), ← rank]

Premises used: Iff.mpr, LinearMap.range_comp_of_range_eq_top, Matrix.rank, LinearMap.range_eq_top, Matrix.mulVecLin_mul
-- 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
suffices : Function.Surjective (α := n → R) (β := n → R) (⇑A.mulVecLin : (a : n → R) → n → R)
⊢ (B * A).rank = B.rank

Tactic:
suffices Function.Surjective A.mulVecLin by
    rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
      (LinearMap.range_eq_top.mpr this), ← rank]
-- 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.mulVecLin : (a : n → R) → n → R) ((A⁻¹.mulVecLin : (a : n → R) → n → R) v : n → R) = v

Tactic:
simp [mul_nonsing_inv _ hA]

Premises used: Matrix.mul_nonsing_inv