awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
M : Matrix (m ⊕ n) (m ⊕ n) R[X] :=
  fromBlocks ((scalar m : (a : R[X]) → Matrix m m R[X]) X) (A.map (⇑C : (a : R) → R[X])) (B.map (⇑C : (a : R) → R[X])) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] :=
  fromBlocks (-1) 0 (B.map (⇑C : (a : R) → R[X])) (-(scalar n : (a : R[X]) → Matrix n n R[X]) X)
hMN :
  M * N =
    fromBlocks
      (HAdd.hAdd (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        (-(scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((A * B).map (⇑C : (a : R) → R[X])))
      (HSMul.hSMul (α := R[X]) (β := Matrix.{u_3, u_4, u_1} m n R[X]) (-X) (A.map (⇑C : (a : R) → R[X]))) 0
      (-(scalar n : (a : R[X]) → Matrix n n R[X]) X)
hNM :
  N * M =
    fromBlocks (-(scalar m : (a : R[X]) → Matrix m m R[X]) X) (-A.map (⇑C : (a : R) → R[X])) 0
      (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
        ((B * A).map (⇑C : (a : R) → R[X]))
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X]))
hdet_MN :
  (M * N).det =
    HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card n) *
        (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
            ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
            ((A * B).map (⇑C : (a : R) → R[X]))).det)
⊢ (N * M).det =
    HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m) *
        (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
            ((B * A).map (⇑C : (a : R) → R[X]))).det)

Tactic:
have hdet_NM : (N * M).det = (-1 : R[X]) ^ (Fintype.card m + Fintype.card n) *
      (X ^ Fintype.card m * (scalar n X - (B * A).map C).det) := by
    rw [hNM, det_fromBlocks_zero₂₁, ← neg_sub, det_neg (_ - _)]
    simp
    ring
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
rw₆ rw₇ :
  HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).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

Tactic:
rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']

Premises used: mul_assoc, Function.Injective.eq_iff, pow_add, Polynomial.isRegular_X_pow, Matrix.charpoly_mul_comm', IsRegular.left, Nat.add_sub_cancel'
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
A B : Matrix n n R
⊢ Eq (α := R[X]) (A * B).charpoly (B * A).charpoly

Tactic:
(isRegular_X_pow _).left.eq_iff.mp <| charpoly_mul_comm' A B

Premises used: Function.Injective.eq_iff, Polynomial.isRegular_X_pow, Iff.mp, Matrix.charpoly_mul_comm', IsRegular.left
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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)
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)
⊢ (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

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 : 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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
⊢ 1 ≤ Fintype.card n

Tactic:
have h : 1 ≤ Fintype.card n := NeZero.one_le
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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)
⊢ (vecMulVec u v).charpoly =
    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]

Premises used: Matrix.charpoly_mul_comm_of_le, Matrix.charmatrix, Matrix.vecMulVec_eq, Unit, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
⊢ 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:
simp [-Matrix.map_mul, mul_sub, ← pow_succ, h, dotProduct_comm, smul_eq_C_mul]

Premises used: mul_sub, pow_succ, Polynomial.smul_eq_C_mul, Matrix.map_mul, dotProduct_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
rw : Eq (α := R[X]) ((↑M : Matrix n n R)⁻¹ * (↑M : Matrix n n R) * N).charpoly N.charpoly
⊢ Eq (α := R[X]) ((↑M : Matrix n n R) * N * (↑M : Matrix n n R)⁻¹).charpoly N.charpoly

Tactic:
rw [Matrix.charpoly_mul_comm, ← mul_assoc]

Premises used: mul_assoc, Matrix.charpoly_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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)⁻¹ * (↑M : Matrix n n R) * N).charpoly N.charpoly

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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

Tactic:
simpa using charpoly_units_conj M⁻¹ N

Premises used: Matrix.charpoly_units_conj, Inv.inv
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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]))))
⊢ (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]))

Tactic:
simp_rw [charpoly, det_apply, Polynomial.sum_comp, Polynomial.smul_comp, Polynomial.prod_comp]

Premises used: Matrix.det_apply, Polynomial.sum_comp, Polynomial.prod_comp, Polynomial.smul_comp, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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]))
⊢ 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:
congr! with σ _ i _
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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]))
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]))
⊢ (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

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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])
⊢ (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:
simp [hi]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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]))

Tactic:
simp [hi]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : Subsingleton R
A : Matrix m n R
⊢ A.cRank = 1

Tactic:
rank_subsingleton _ _

Premises used: Matrix.cRank, rank_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
A : Matrix m n R
⊢ (toNat : (a : Cardinal.{max uR um}) → ℕ) A.cRank = finrank R ↥(span R (range A.col))

Tactic:
rfl

Premises used: Set.Mem, setOf, Matrix.cRank, Matrix.col, Module.finrank, rfl
-- 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
x : n₀
⊢ ((A.submatrix r id).submatrix id c)ᵀ x ∈ range (A.submatrix r id)ᵀ

Tactic:
⟨c x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- 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
x : n₀
⊢ ((A.submatrix r id).submatrix id c)ᵀ x ∈ range (A.submatrix r id)ᵀ

Tactic:
exact ⟨c x, rfl⟩
-- 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 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⟩
-- 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
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

Tactic:
(Cardinal.lift_monotone h).trans ?_

Premises used: Matrix.submatrix, Cardinal.lift_monotone, LE.le.trans
-- 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
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
refine : lift.{um, max uR um₀} (A.submatrix r id).cRank ≤ lift.{um₀, max uR um} A.cRank
⊢ lift.{um, max uR um₀} (A.submatrix r c).cRank ≤ lift.{um₀, max uR um} A.cRank

Tactic:
refine (Cardinal.lift_monotone h).trans ?_

Premises used: Cardinal.lift_monotone, LE.le.trans
-- 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
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
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)))
⊢ Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ)

Tactic:
rw [LinearMap.map_span, ← image_univ, image_image, transpose_submatrix]

Premises used: Set.image_image, Set.image_univ, Matrix.transpose_submatrix, LinearMap.map_span
-- 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
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
⊢ 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:
aesop
-- 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
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)ᵀ)

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
-- 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
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)ᵀ)
rw : lift.{um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤ lift.{um₀, max uR um} A.cRank
⊢ lift.{um, max uR um₀} (A.submatrix r id).cRank ≤ lift.{um₀, max uR um} A.cRank

Tactic:
rw [cRank, ← h_eq]

Premises used: Matrix.cRank
-- 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
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.{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ᵀ))
-- 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
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ᵀ)))
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
⊢ lift.{um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤ lift.{um₀, max uR um} A.cRank

Tactic:
simp_rw [← lift_umax] at hwin ⊢

Premises used: Cardinal.lift_umax
-- 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
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 (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:
hwin

Premises used: Set.Mem, setOf, Matrix.cRank
-- 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
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 (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:
exact hwin
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
n : Type un
n₀ : Type un₀
R : Type uR
inst : Semiring R
m m₀ : Type um
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).cRank ≤ A.cRank

Tactic:
simpa using lift_cRank_submatrix_le A r c

Premises used: Matrix.lift_cRank_submatrix_le
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
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
rw rw₁ :
  LE.le (α := Cardinal.{max um uR}) (↑(Fintype.card m) : Cardinal.{max uR um})
    (↑(Fintype.card m) : Cardinal.{max uR um})
⊢ Module.rank R (m → R) ≤ (↑(Fintype.card m) : Cardinal.{max uR um})

Tactic:
rw [rank_fun']

Premises used: rank_fun'
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype n
A : Matrix m n R
⊢ #(↑(range Aᵀ) : Type (max uR um)) ≤ (↑(Fintype.card n) : Cardinal.{max uR um})

Tactic:
simpa using Cardinal.mk_range_le_lift (f := Aᵀ)

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
inst_1 : Subsingleton R
A : Matrix m n R
⊢ A.eRank = 1

Tactic:
simp [eRank]

Premises used: Matrix.eRank
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
m : Type um
n : Type un
R : Type uR
inst : Semiring R
A : Matrix m n R
⊢ A.eRank.toNat = finrank R ↥(span R (range A.col))

Tactic:
toNat_toENat ..

Premises used: Set.Mem, Matrix.eRank, setOf, Matrix.cRank, Cardinal.toNat_toENat, Matrix.col, Module.finrank