awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
A : Matrix m n R
B : Matrix n m R
hle : Fintype.card n ≤ Fintype.card m
rw :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly)
rw₁ : ℕ
rw₂ :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) * HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) *
      (B * A).charpoly
rw₃ : ℕ
rw₄ :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n + (Fintype.card m - Fintype.card n)) * (B * A).charpoly
m₁ : ℕ
rw₅ :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly
⊢ (A * B).charpoly = HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly
have rw₆ : HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly =
  HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly
Tactic: rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
u v : n → R
⊢ (vecMulVec u v).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
have inl : IsEmpty n →
  (vecMulVec u v).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
u v : n → R
inl :
  IsEmpty n →
    (vecMulVec u v).charpoly =
      HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
⊢ (vecMulVec u v).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
have inr : Nonempty n →
  (vecMulVec u v).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
u v : n → R
h : Nonempty n
⊢ (vecMulVec u v).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
have h : 1 ≤ Fintype.card n
Tactic: have h : 1 ≤ Fintype.card n := NeZero.one_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
u v : n → R
h_1 : Nonempty n
h : 1 ≤ Fintype.card n
⊢ (vecMulVec u v).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
have inr : HPow.hPow (α := R[X]) X (Fintype.card n - Fintype.card Unit) *
    (HSub.hSub (α := Matrix Unit Unit R[X]) (β := Matrix Unit Unit R[X])
        ((scalar Unit : (a : R[X]) → Matrix Unit Unit R[X]) X : Matrix Unit Unit R[X])
        ((RingHom.mapMatrix C : (a : Matrix Unit Unit R) → Matrix Unit Unit R[X])
            (replicateRow Unit v * replicateCol Unit u) :
          Matrix Unit Unit R[X])).det =
  HPow.hPow (α := R[X]) X (Fintype.card n) - (u ⬝ᵥ v) • HPow.hPow (α := R[X]) X (Fintype.card n - 1)
Tactic: rw [vecMulVec_eq (ι := Unit), charpoly_mul_comm_of_le (n := Unit) _ _ h, charpoly, charmatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ Eq (α := R[X]) ((↑M : Matrix n n R) * N * (↑M : Matrix n n R)⁻¹).charpoly N.charpoly
have rw : Eq (α := R[X]) ((↑M : Matrix n n R)⁻¹ * (↑M : Matrix n n R) * N).charpoly N.charpoly
Tactic: rw [Matrix.charpoly_mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
μ : R
⊢ (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charpoly =
    Polynomial.comp M.charpoly (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
have simp_rw : Eq.{u_1 + 1} (α := R[X])
  (∑ σ : Equiv.Perm n,
    HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
      (∏ i : n,
        (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
          ((σ : (a : n) → n) i) i))
  (∑ x : Equiv.Perm n,
    HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
      (∏ j : n,
        Polynomial.comp (M.charmatrix ((x : (a : n) → n) j) j)
          (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))))
Tactic: simp_rw [charpoly, det_apply, Polynomial.sum_comp, Polynomial.smul_comp, Polynomial.prod_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
μ : R
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n,
          (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
            ((σ : (a : n) → n) i) i))
    (∑ x : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
        (∏ j : n,
          Polynomial.comp (M.charmatrix ((x : (a : n) → n) j) j)
            (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))))
have a : ∀ (σ : Equiv.Perm n),
  Membership.mem (γ := Finset (Equiv.Perm n)) univ σ →
    ∀ (i : n),
      Membership.mem (γ := Finset n) univ i →
        (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
            ((σ : (a : n) → n) i) i =
          Polynomial.comp (M.charmatrix ((σ : (a : n) → n) i) i)
            (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
Tactic: congr! with σ _ i _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
μ : R
σ : Equiv.Perm n
h : Membership.mem (γ := Finset (Equiv.Perm n)) univ σ
i : n
h_1 : Membership.mem (γ := Finset n) univ i
⊢ (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
      ((σ : (a : n) → n) i) i =
    Polynomial.comp (M.charmatrix ((σ : (a : n) → n) i) i)
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
have pos : ∀ (hi : (σ : (a : n) → n) i = i),
  (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
      ((σ : (a : n) → n) i) i =
    Polynomial.comp (M.charmatrix ((σ : (a : n) → n) i) i)
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
Tactic: by_cases hi : σ i = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
μ : R
σ : Equiv.Perm n
h : Membership.mem (γ := Finset (Equiv.Perm n)) univ σ
i : n
h_1 : Membership.mem (γ := Finset n) univ i
pos :
  ∀ (hi : (σ : (a : n) → n) i = i),
    (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
        ((σ : (a : n) → n) i) i =
      Polynomial.comp (M.charmatrix ((σ : (a : n) → n) i) i)
        (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
⊢ (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
      ((σ : (a : n) → n) i) i =
    Polynomial.comp (M.charmatrix ((σ : (a : n) → n) i) i)
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
have neg : ∀ (hi : ¬(σ : (a : n) → n) i = i),
  (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
      ((σ : (a : n) → n) i) i =
    Polynomial.comp (M.charmatrix ((σ : (a : n) → n) i) i)
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
Tactic: by_cases hi : σ i = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
μ : R
σ : Equiv.Perm n
h : Membership.mem (γ := Finset (Equiv.Perm n)) univ σ
i : n
h_1 : Membership.mem (γ := Finset n) univ i
hi : (σ : (a : n) → n) i = i
⊢ (HSub.hSub (β := Matrix n n R) M ((scalar n : (a : R) → Matrix n n R) μ : Matrix n n R)).charmatrix
      ((σ : (a : n) → n) i) i =
    Polynomial.comp (M.charmatrix ((σ : (a : n) → n) i) i)
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
have pos : X - HSub.hSub (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (M i i) : R[X]) ((C : (a : R) → R[X]) μ : R[X]) =
  HSub.hSub (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))
    ((C : (a : R) → R[X]) (M i i) : R[X])
Tactic: simp [hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ lift.{um, max uR um₀} (A.submatrix r c).cRank ≤ lift.{um₀, max uR um} A.cRank
have h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
Tactic: have h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank :=
    Submodule.rank_mono <| span_mono <| by rintro _ ⟨x, rfl⟩; exact ⟨c x, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
⊢ lift.{um, max uR um₀} (A.submatrix r c).cRank ≤ lift.{um₀, max uR um} A.cRank
have refine : lift.{um, max uR um₀} (A.submatrix r id).cRank ≤ lift.{um₀, max uR um} A.cRank
Tactic: refine (Cardinal.lift_monotone h).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ)
have rw : Eq (α := Submodule R (m₀ → R)) (span R ((fun (x : n) ↦ (f : (a : m → R) → m₀ → R) (Aᵀ x)) '' Set.univ))
  (span R (range (Aᵀ.submatrix id r)))
Tactic: rw [LinearMap.map_span, ← image_univ, image_image, transpose_submatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ lift.{um, max uR um₀} (A.submatrix r id).cRank ≤ lift.{um₀, max uR um} A.cRank
have h_eq : Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ)
Tactic: have h_eq : Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ) := by
    rw [LinearMap.map_span, ← image_univ, image_image, transpose_submatrix]
    aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
h_eq : Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ)
⊢ lift.{um, max uR um₀} (A.submatrix r id).cRank ≤ lift.{um₀, max uR um} A.cRank
have rw : lift.{um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤ lift.{um₀, max uR um} A.cRank
Tactic: rw [cRank, ← h_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
h_eq : Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ)
⊢ lift.{um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤ lift.{um₀, max uR um} A.cRank
have hwin : lift.{max uR um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤
  lift.{max uR um₀, max uR um} (Module.rank R ↥(span R (range Aᵀ)))
Tactic: have hwin := lift_rank_map_le f (span R (range Aᵀ))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
h_eq : Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ)
hwin :
  lift.{max uR um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤
    lift.{max uR um₀, max uR um} (Module.rank R ↥(span R (range Aᵀ)))
⊢ lift.{um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤ lift.{um₀, max uR um} A.cRank
have simp_rw : ∀
  (hwin :
    lift.{max (max uR um₀) (max uR um) um₀, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤
      lift.{max (max uR um) um₀, max uR um} (Module.rank R ↥(span R (range Aᵀ)))),
  lift.{max (max uR um₀) (max uR um) um₀, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤
    lift.{max (max uR um) um₀, max uR um} A.cRank
Tactic: simp_rw [← lift_umax] at hwin ⊢
Cleared hypotheses: hwin
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype m
A : Matrix m n R
⊢ Module.rank R (m → R) ≤ (↑(Fintype.card m) : Cardinal.{max uR um})
have rw : LE.le (α := Cardinal.{max um uR}) (↑(Fintype.card m) : Cardinal.{max uR um}) (↑(Fintype.card m) : Cardinal.{max uR um})
Tactic: rw [rank_fun']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
⊢ A.eRank ≤ ENat.card n
have 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
Tactic: wlog hfin : Finite n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.eRank ≤ ENat.card n
have 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
Tactic: wlog hfin : Finite n
Cleared hypotheses: inst_1, A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.eRank ≤ ENat.card n
have have : ∀ (x : Fintype n), A.eRank ≤ ENat.card n
Tactic: have _ := Fintype.ofFinite n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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.eRank ≤ ENat.card n
have rw : A.cRank ≤ (↑(Fintype.card n) : Cardinal.{max uR um})
Tactic: rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
⊢ A.eRank ≤ ENat.card m
have 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
Tactic: wlog hfin : Finite m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.eRank ≤ ENat.card m
have 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
Tactic: wlog hfin : Finite m
Cleared hypotheses: inst_1, A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.eRank ≤ ENat.card m
have have : ∀ (x : Fintype m), A.eRank ≤ ENat.card m
Tactic: have _ := Fintype.ofFinite m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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.eRank ≤ ENat.card m
have rw : A.cRank ≤ (↑(Fintype.card m) : Cardinal.{max uR um})
Tactic: rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
A : Matrix m n R
⊢ A.eRank ≤ ENat.card m
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.eRank ≤ ENat.card m
have 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
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
Cleared hypotheses: inst_1, A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.eRank ≤ ENat.card m
have 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
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
Cleared hypotheses: inst_1, A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ A.eRank ≤ ENat.card m
have 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})
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
Cleared hypotheses: inst_1, A
-- 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
⊢ LinearIndependent (ι := m) R (M := m → R) 1ᵀ
have h : ∀ (x : m), Eq (α := m → R) (1ᵀ x) (Pi.single (M := fun (i : m) ↦ R) x 1)
Tactic: convert! Pi.linearIndependent_single_one m R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
Goal:
m : Type um
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq m
⊢ cRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = lift.{uR, um} #m
have h : 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]
-- 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ᵀ
⊢ cRank.{um, um, uR} (m := m) (n := m) (R := R) 1 = lift.{uR, um} #m
have rw : Module.rank R ↥(span R (range (ι := m) 1ᵀ)) = lift.{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
⊢ 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.{uR, um} #m
Tactic: rw [cRank, rank_span h, ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']