awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), (abv : (a : R) → S) (A i j) ≤ x
i : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ i
i_1 : n
h_1 : Membership.mem (γ := Finset n) univ i_1
⊢ (abv : (a : R) → S) (A ((i : (a : n) → n) i_1) i_1) ≤ x

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), (abv : (a : R) → S) (A i j) ≤ x
⊢ ∑ _σ : Perm n, ∏ _i : n, x = (Fintype.card n)! • x ^ Fintype.card n

Tactic:
simp [Fintype.card_perm]

Premises used: Fintype.card_perm
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), (abv : (a : R) → S) (A k i j) ≤ x
i j : n
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) ((∑ k ∈ s, A k) i j) : S) ((abv : (a : R) → S) (∑ k ∈ s, A k i j) : S)

Tactic:
simp only [sum_apply]

Premises used: Matrix.sum_apply
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), (abv : (a : R) → S) (A k i j) ≤ x
i j : n
h : ∀ i_1 ∈ s, (abv : (a : R) → S) (A i_1 i j) ≤ x
⊢ LE.le.{u_2} (α := S) (∑ k ∈ s, (abv : (a : R) → S) (A k i j)) (∑ _k ∈ s, x)

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), (abv : (a : R) → S) (A k i j) ≤ x
i j : n
i_1 : ι
h : i_1 ∈ s
⊢ (abv : (a : R) → S) (A i_1 i j) ≤ x

Tactic:
apply hx
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
ι : Type u_4
s : Finset ι
c : ι → R
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), (abv : (a : R) → S) (A k i j) ≤ x
y : S
hy : ∀ (k : ι), (abv : (a : R) → S) (c k) ≤ y
⊢ (abv : (a : R) → S) (det.{u_1, u_3} (n := n) (∑ k ∈ s, c k • A k)) ≤ (Fintype.card n)! • (#s • y * x) ^ Fintype.card n

Tactic:
simpa only [smul_mul_assoc] using
    det_sum_le s fun k i j =>
      calc
        abv (c k * A k i j) = abv (c k) * abv (A k i j) := abv.map_mul _ _
        _ ≤ y * x := mul_le_mul (hy k) (hx k i j) (abv.nonneg _) ((abv.nonneg _).trans (hy k))

Premises used: Trans.trans, Matrix.det_sum_le, smul_mul_assoc, AbsoluteValue.nonneg, mul_le_mul, LE.le.trans, AbsoluteValue.map_mul
-- 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
i j : n
⊢ M.charmatrix i j =
    HSub.hSub (α := R[X]) (β := R[X]) (diagonal (fun (x : n) ↦ X) i j : R[X]) ((C : (a : R) → R[X]) (M i j) : R[X])

Tactic:
rfl

Premises used: Matrix.charmatrix, Matrix.map, Polynomial.X, Matrix.diagonal, rfl, ite
-- 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
i : n
⊢ M.charmatrix i i = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])

Tactic:
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, map_apply,
    diagonal_apply_eq]

Premises used: RingHom.mapMatrix_apply, Matrix.diagonal_apply_eq, Matrix.sub_apply, Matrix.map_apply, Matrix.charmatrix, Matrix.scalar_apply
-- 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
i j : n
h : i ≠ j
⊢ Eq (α := R[X]) (M.charmatrix i j) (-(C : (a : R) → R[X]) (M i j))

Tactic:
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, diagonal_apply_ne _ h,
    map_apply, sub_eq_neg_self]

Premises used: RingHom.mapMatrix_apply, Matrix.sub_apply, Matrix.map_apply, Matrix.charmatrix, sub_eq_neg_self, Matrix.scalar_apply, Matrix.diagonal_apply_ne
-- 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
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (charmatrix 0) ((scalar n : (a : R[X]) → Matrix n n R[X]) X)

Tactic:
simp [charmatrix]

Premises used: Matrix.charmatrix
-- 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
d : n → R
rw :
  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])
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₁ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₂ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X) ((diagonal d).map (⇑C : (a : R) → R[X])) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₃ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
      (diagonal fun (m : n) ↦ (C : (a : R) → R[X]) (d m)) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₄ rw₅ :
  Eq (α := Matrix.{u_4, u_4, u_1} n n R[X])
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal d).charmatrix
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))

Tactic:
rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]

Premises used: RingHom.mapMatrix_apply, Matrix.charmatrix, map_zero, Matrix.diagonal_sub, Matrix.scalar_apply, Matrix.diagonal_map
-- 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
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (charmatrix 1) (diagonal fun (x : n) ↦ HSub.hSub (α := R[X]) X 1)

Tactic:
charmatrix_diagonal _

Premises used: Matrix.charmatrix_diagonal
-- 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
k : ℕ
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (charmatrix (↑k : Matrix n n R))
    (diagonal fun (x : n) ↦ HSub.hSub (α := R[X]) X (↑k : R[X]))

Tactic:
charmatrix_diagonal _

Premises used: Matrix.charmatrix_diagonal, Finsupp.single
-- 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
k : ℕ
inst_3 : k.AtLeastTwo
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (charmatrix (OfNat.ofNat k))
    (diagonal fun (x : n) ↦ HSub.hSub (α := R[X]) X (OfNat.ofNat k))

Tactic:
charmatrix_natCast _

Premises used: Matrix.charmatrix_natCast
-- 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
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) Mᵀ.charmatrix M.charmatrixᵀ

Tactic:
simp [charmatrix, transpose_map]

Premises used: Matrix.charmatrix, Matrix.transpose_map
-- 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
a :
  ∀ (k : ℕ) (i j : n),
    coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M.charmatrix) k i j =
      (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
            ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])).coeff
        k i j
⊢ (matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M.charmatrix =
    HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
      ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])

Tactic:
ext k i j
-- 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
k : ℕ
i j : n
a :
  coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M.charmatrix) k i j =
    (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
          ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])).coeff
      k i j

Tactic:
simp only [matPolyEquiv_coeff_apply, coeff_sub]

Premises used: Polynomial.coeff_sub, matPolyEquiv_coeff_apply
-- 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
k : ℕ
i j : n
pos :
  ∀ (h : i = j),
    coeff (M.charmatrix i j) k =
      HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
        (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
neg :
  ∀ (h : ¬i = j),
    coeff (M.charmatrix i j) k =
      HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
        (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
⊢ coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j

Tactic:
by_cases h : i = j
-- 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
k : ℕ
i j : n
h : i = j
pos :
  coeff (M.charmatrix i i) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i
⊢ coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j

Tactic:
subst h
-- 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
k : ℕ
i : n
pos :
  HSub.hSub (α := R) (coeff X k) (coeff ((C : (a : R) → R[X]) (M i i)) k) =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i
⊢ coeff (M.charmatrix i i) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i

Tactic:
rw [charmatrix_apply_eq, coeff_sub]

Premises used: Matrix.charmatrix_apply_eq, Polynomial.coeff_sub
-- 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
k : ℕ
i : n
pos :
  ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) =
    HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i i
⊢ HSub.hSub (α := R) (coeff X k) (coeff ((C : (a : R) → R[X]) (M i i)) k) =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i

Tactic:
simp only [coeff_X, coeff_C]

Premises used: Polynomial.coeff_C, Polynomial.coeff_X
-- 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
k : ℕ
i : n
pos : 1 = k → k = 0 → 1 - M i i = HSub.hSub (α := Matrix n n R) 1 M i i
neg : 1 = k → ¬k = 0 → HSub.hSub (α := R) 1 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i i
pos₁ : ¬1 = k → k = 0 → 0 - M i i = HSub.hSub (α := Matrix n n R) 0 M i i
neg₁ : ¬1 = k → ¬k = 0 → HSub.hSub (α := R) 0 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 0 0 i i
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) =
    HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i i

Tactic:
split_ifs
-- 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
k : ℕ
i : n
h : 1 = k
h_1 : k = 0
⊢ 1 - M i i = HSub.hSub (α := Matrix n n R) 1 M i i

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
k : ℕ
i : n
h : 1 = k
h_1 : ¬k = 0
⊢ HSub.hSub (α := R) 1 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i i

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
k : ℕ
i : n
h : ¬1 = k
h_1 : k = 0
⊢ 0 - M i i = HSub.hSub (α := Matrix n n R) 0 M i i

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
k : ℕ
i : n
h : ¬1 = k
h_1 : ¬k = 0
⊢ HSub.hSub (α := R) 0 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 0 0 i i

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
k : ℕ
i j : n
h : ¬i = j
neg :
  (-if k = 0 then M i j else 0) = HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i j
⊢ coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j

Tactic:
rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]

Premises used: Matrix.charmatrix_apply_ne, Polynomial.coeff_C, Polynomial.coeff_neg, Polynomial.coeff_X
-- 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
k : ℕ
i j : n
h : ¬i = j
pos : k = 0 → 1 = k → -M i j = HSub.hSub (α := Matrix n n R) 1 M i j
neg : k = 0 → ¬1 = k → -M i j = HSub.hSub (α := Matrix n n R) 0 M i j
pos₁ : ¬k = 0 → 1 = k → -0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i j
neg₁ : ¬k = 0 → ¬1 = k → -0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 0 0 i j
⊢ (-if k = 0 then M i j else 0) = HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i j

Tactic:
split_ifs
-- 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
k : ℕ
i j : n
h : ¬i = j
h_1 : k = 0
h_2 : 1 = k
⊢ -M i j = HSub.hSub (α := Matrix n n R) 1 M i j

Tactic:
simp [h]
-- 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
k : ℕ
i j : n
h : ¬i = j
h_1 : k = 0
h_2 : ¬1 = k
⊢ -M i j = HSub.hSub (α := Matrix n n R) 0 M i j

Tactic:
simp [h]
-- 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
k : ℕ
i j : n
h : ¬i = j
h_1 : ¬k = 0
h_2 : 1 = k
⊢ -0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i j

Tactic:
simp [h]
-- 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
k : ℕ
i j : n
h : ¬i = j
h_1 : ¬k = 0
h_2 : ¬1 = k
⊢ -0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 0 0 i j

Tactic:
simp [h]
-- 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
M : Matrix n n R
e : n ≃ m
a :
  ∀ (i j : m) (x : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
      (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
⊢ Eq (α := Matrix.{u_3, u_3, u_1} m m R[X]) (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M))
    ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix)

Tactic:
ext i j x
-- 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
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
pos :
  ∀ (h : i = j),
    Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
      (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
neg :
  ∀ (h : ¬i = j),
    Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
      (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
⊢ Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)

Tactic:
by_cases h : i = j
-- 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
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : i = j
⊢ Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)

Tactic:
simp [h]
-- 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
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : ¬i = j
⊢ Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
a :
  ∀ (i j : n) (n_1 : ℕ),
    coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
⊢ charmatrix (M.map (⇑f : (a : R) → S)) = map M.charmatrix (Polynomial.map f)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n_1 : ℕ
pos :
  ∀ (h : i = j),
    coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
neg :
  ∀ (h : ¬i = j),
    coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
⊢ coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1

Tactic:
by_cases h : i = j
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n_1 : ℕ
h : i = j
⊢ coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1

Tactic:
simp [h, charmatrix, diagonal]

Premises used: Matrix.charmatrix, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n_1 : ℕ
h : ¬i = j
⊢ coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1

Tactic:
simp [h, charmatrix, diagonal]

Premises used: Matrix.charmatrix, Matrix.diagonal
-- 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
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i j : m
n_1 : ℕ
⊢ (HSub.hSub (α := Matrix (m ⊕ n) (m ⊕ n) R[X]) (β := Matrix (m ⊕ n) (m ⊕ n) R[X])
          ((scalar (m ⊕ n) : (a : R[X]) → Matrix (m ⊕ n) (m ⊕ n) R[X]) X : Matrix (m ⊕ n) (m ⊕ n) R[X])
          ((RingHom.mapMatrix C : (a : Matrix (m ⊕ n) (m ⊕ n) R) → Matrix (m ⊕ n) (m ⊕ n) R[X])
              (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) :
            Matrix (m ⊕ n) (m ⊕ n) R[X])
          (Sum.inl i) (Sum.inl j)).coeff
      n_1 =
    (fromBlocks
          (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])
            ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M₁₁ : Matrix.{u_3, u_3, u_1} m m R[X]))
          (-M₁₂.map (⇑C : (a : R) → R[X])) (-M₂₁.map (⇑C : (a : R) → R[X]))
          (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])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M₂₂ : Matrix.{u_4, u_4, u_1} n n R[X]))
          (Sum.inl i) (Sum.inl j)).coeff
      n_1

Tactic:
simp [diagonal]

Premises used: Matrix.diagonal