awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = lift.{uR, um} #m
have rw₂ : #(↑(range (ι := m) 1ᵀ) : Type (max uR um)) = lift.{max um uR, um} #m
Tactic: rw [cRank, rank_span h, ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = lift.{uR, um} #m
have rw₃ : #(↑(range (ι := m) 1ᵀ) : Type (max uR um)) = lift.{um, max uR um} #(↑(range (ι := m) 1ᵀ) : Type (max uR um))
Tactic: rw [cRank, rank_span h, ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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))
⊢ cRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = lift.{uR, um} #m
have rw₄ : #(↑(range (ι := m) 1ᵀ) : Type (max uR um)) = #(↑(range (ι := m) 1ᵀ) : Type (max uR um))
Tactic: rw [cRank, rank_span h, ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
⊢ eRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = ENat.card m
have rw : (toENat : (a : Cardinal.{max uR um}) → ℕ∞) (cRank.{um, um, uR} (m := m) (n := m) (R := R) 1) = ENat.card m
Tactic: rw [eRank, cRank_one, toENat_lift, ENat.card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ eRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = ENat.card m
have rw₁ : (toENat : (a : Cardinal.{max uR um}) → ℕ∞) (lift.{uR, um} #m) = ENat.card m
Tactic: rw [eRank, cRank_one, toENat_lift, ENat.card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ eRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = ENat.card m
have rw₂ : (toENat : (a : Cardinal.{um}) → ℕ∞) #m = ENat.card m
Tactic: rw [eRank, cRank_one, toENat_lift, ENat.card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ eRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = ENat.card m
have rw₃ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{um}) → ℕ∞) #m : ℕ∞) ((toENat : (a : Cardinal.{um}) → ℕ∞) #m : ℕ∞)
Tactic: rw [eRank, cRank_one, toENat_lift, ENat.card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
n : Type un
R : Type uR
inst : Fintype n
inst_1 : CommRing R
inst_2 : Nontrivial R
inst_3 : DecidableEq n
⊢ rank.{un, un, uR} (m := n) (n := n) (R := R) 1 = Fintype.card n
have rw : finrank R ↥(LinearMap.range (M := n → R) (mulVecLin 1)) = Fintype.card n
Tactic: rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ rank.{un, un, uR} (m := n) (n := n) (R := R) 1 = Fintype.card n
have rw₁ : finrank R ↥(LinearMap.range LinearMap.id) = Fintype.card n
Tactic: rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ rank.{un, un, uR} (m := n) (n := n) (R := R) 1 = Fintype.card n
have rw₂ : finrank R ↥⊤ = Fintype.card n
Tactic: rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ rank.{un, un, uR} (m := n) (n := n) (R := R) 1 = Fintype.card n
have rw₃ : finrank R (n → R) = Fintype.card n
Tactic: rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ rank.{un, un, uR} (m := n) (n := n) (R := R) 1 = Fintype.card n
have rw₄ : Fintype.card n = Fintype.card n
Tactic: rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]
-- 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 : Nontrivial R
⊢ rank.{um, un, uR} (m := m) (n := n) (R := R) 0 = 0
have rw : finrank R ↥(LinearMap.range (M := n → R) (mulVecLin 0)) = 0
Tactic: rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]
-- 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 : Nontrivial R
rw : finrank R ↥(LinearMap.range (M := n → R) (mulVecLin 0)) = 0
⊢ rank.{um, un, uR} (m := m) (n := n) (R := R) 0 = 0
have rw₁ : finrank R ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R) 0) = 0
Tactic: rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]
-- 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 : 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
⊢ rank.{um, un, uR} (m := m) (n := n) (R := R) 0 = 0
have rw₂ : finrank R ↥⊥ = 0
Tactic: rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]
-- 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 : 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
⊢ rank.{um, un, uR} (m := m) (n := n) (R := R) 0 = 0
have rw₃ : Eq (α := ℕ) 0 0
Tactic: rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
R : Type uR
inst : CommRing R
m : Type u_1
n : Type u_2
inst_1 : Nontrivial R
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inl : ∀ (hn : IsEmpty n), cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
Tactic: obtain hn | hn := isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inr : ∀ (hn : Nonempty n), cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
Tactic: obtain hn | hn := isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
R : Type uR
inst : CommRing R
m : Type u_1
n : Type u_2
inst_1 : Nontrivial R
hn : IsEmpty n
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inl : Module.rank R ↥(span R (range (ι := n) 0ᵀ)) = 0
Tactic: rw [cRank, range_eq_empty, span_empty, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inl₁ : Module.rank R ↥(span R ∅) = 0
Tactic: rw [cRank, range_eq_empty, span_empty, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inl₂ : Module.rank R ↥⊥ = 0
Tactic: rw [cRank, range_eq_empty, span_empty, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inl₃ : Eq (α := Cardinal.{max uR u_1}) 0 0
Tactic: rw [cRank, range_eq_empty, span_empty, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
R : Type uR
inst : CommRing R
m : Type u_1
n : Type u_2
inst_1 : Nontrivial R
hn : Nonempty n
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inr : Module.rank R ↥(span R (range (ι := n) 0ᵀ)) = 0
Tactic: rw [cRank, transpose_zero, range_zero, span_zero_singleton, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inr₁ : Module.rank R ↥(span R (range (ι := n) 0)) = 0
Tactic: rw [cRank, transpose_zero, range_zero, span_zero_singleton, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inr₂ : Module.rank R ↥(R ∙ 0) = 0
Tactic: rw [cRank, transpose_zero, range_zero, span_zero_singleton, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inr₃ : Module.rank R ↥⊥ = 0
Tactic: rw [cRank, transpose_zero, range_zero, span_zero_singleton, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ cRank.{u_1, u_2, uR} (m := m) (n := n) (R := R) 0 = 0
have inr₄ : Eq (α := Cardinal.{max uR u_1}) 0 0
Tactic: rw [cRank, transpose_zero, range_zero, span_zero_singleton, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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 ≤ A.rank
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ (A * B).rank ≤ A.rank
have rw : finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range A.mulVecLin)
Tactic: rw [rank, rank, mulVecLin_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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 ≤ B.rank
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ (A * B).rank ≤ B.rank
have rw : finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥(LinearMap.range B.mulVecLin)
Tactic: rw [rank, rank, mulVecLin_mul]
-- 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
w : m → R
v : n → R
⊢ (vecMulVec w v).rank ≤ 1
have rw : (replicateCol Unit w * replicateRow Unit v).rank ≤ 1
Tactic: rw [Matrix.vecMulVec_eq Unit]
-- 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
w : m → R
v : n → R
⊢ (replicateCol Unit w * replicateRow Unit v).rank ≤ 1
have refine : (replicateCol Unit w).rank ≤ 1
Tactic: refine le_trans (rank_mul_le_left _ _) ?_
-- 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
w : m → R
v : n → R
⊢ (replicateCol Unit w).rank ≤ 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
have apply : Fintype.card n ≤ (↑A : Matrix n n R).rank
Tactic: apply le_antisymm (rank_le_card_width (A : Matrix n n R)) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
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)ˣ
⊢ Fintype.card n ≤ (↑A : Matrix n n R).rank
have this : ((↑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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ Fintype.card n ≤ (↑A : Matrix n n R).rank
have rwa : ∀ (this : (↑(A * A⁻¹) : Matrix n n R).rank ≤ (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ Fintype.card n ≤ (↑A : Matrix n n R).rank
have 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
Tactic: rwa [← Units.val_mul, mul_inv_cancel, Units.val_one, rank_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ Fintype.card n ≤ (↑A : Matrix n n R).rank
have 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
Tactic: rwa [← Units.val_mul, mul_inv_cancel, Units.val_one, rank_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ Fintype.card n ≤ (↑A : Matrix n n R).rank
have rwa₃ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.rank = Fintype.card n
have obtain : ∀ (A : (Matrix n n R)ˣ), (↑A : Matrix n n R).rank = Fintype.card n
Tactic: obtain ⟨A, rfl⟩ := h
Cleared hypotheses: A, h
-- 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 : 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)
⊢ (B * A).rank = B.rank
have rw : finrank R ↥(LinearMap.range (B * A).mulVecLin) = B.rank
Tactic: rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
      (LinearMap.range_eq_top.mpr this), ← 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 : 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
⊢ (B * A).rank = B.rank
have rw₁ : finrank R ↥(B.mulVecLin ∘ₗ A.mulVecLin).range = B.rank
Tactic: rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
      (LinearMap.range_eq_top.mpr this), ← 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 : 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
⊢ (B * A).rank = B.rank
have rw₂ : finrank R ↥(LinearMap.range B.mulVecLin) = B.rank
Tactic: rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
      (LinearMap.range_eq_top.mpr this), ← 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 : 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
⊢ (B * A).rank = B.rank
have rw₃ : B.rank = B.rank
Tactic: rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
      (LinearMap.range_eq_top.mpr this), ← 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 : CommRing R
inst_2 : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
⊢ (B * A).rank = B.rank
have suffices : Function.Surjective (α := n → R) (β := n → R) (⇑A.mulVecLin : (a : n → R) → n → R)
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]
-- 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
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ IsUnit.{uR} (M := R)
    (det.{uR, um} (n := m) ((LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin))
have h : (LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin = A
Tactic: convert! hA
-- 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
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ (LinearMap.toMatrix b b : (a : (m → R) →ₗ[R] m → R) → Matrix m m R) A.mulVecLin = A
have h : Eq (α := (m → R) →ₗ[R] m → R) A.mulVecLin (((LinearMap.toMatrix b b).symm : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) A)
Tactic: rw [← LinearEquiv.eq_symm_apply]
-- 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
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ (A * B).rank = B.rank
have 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))
Tactic: replace hA : IsUnit (LinearMap.toMatrix b b A.mulVecLin).det := by
    convert! hA; rw [← LinearEquiv.eq_symm_apply]; rfl
Cleared hypotheses: hA