awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
⊢ Eq.{u_2 + 1} (α := α)
    (∑ b : Equiv.Perm n,
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) b : ℤˣ)
            (∏ i : n,
              HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                (B.map (⇑C : (a : α) → α[X])) ((b : (a : n) → n) i) i)).coeff
        0)
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, B ((σ : (a : n) → n) i) i))

Tactic:
Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
refine :
  ∀ (x : Equiv.Perm n),
    Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ x →
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
              (∏ i : n,
                HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                  (B.map (⇑C : (a : α) → α[X])) ((x : (a : n) → n) i) i)).coeff
          0 =
        HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
          (∏ i : n, B ((x : (a : n) → n) i) i)
⊢ Eq.{u_2 + 1} (α := α)
    (∑ b : Equiv.Perm n,
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) b : ℤˣ)
            (∏ i : n,
              HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                (B.map (⇑C : (a : α) → α[X])) ((b : (a : n) → n) i) i)).coeff
        0)
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, B ((σ : (a : n) → n) i) i))

Tactic:
refine Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
          (∏ i : n,
            HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)).coeff
      0 =
    HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
      (coeff
        (∏ i : n,
          HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
        0)

Tactic:
coeff_smul (R := α) (sign g) _ 0

Premises used: Equiv.Perm.sign, Polynomial.coeff_smul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
h :
  Eq.{u_2 + 1} (α := α) (∏ i : n, B ((g : (a : n) → n) i) i)
    (coeff
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
      0)
⊢ (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
          (∏ i : n,
            HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)).coeff
      0 =
    HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
      (∏ i : n, B ((g : (a : n) → n) i) i)

Tactic:
convert! coeff_smul (R := α) (sign g) _ 0

Premises used: Equiv.Perm.sign, Polynomial.coeff_smul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
h :
  Eq.{u_2 + 1} (α := α) (∏ i : n, B ((g : (a : n) → n) i) i)
    (∏ i : n,
      (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i).coeff
        0)
⊢ Eq.{u_2 + 1} (α := α) (∏ i : n, B ((g : (a : n) → n) i) i)
    (coeff
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
      0)

Tactic:
rw [coeff_zero_prod]

Premises used: Polynomial.coeff_zero_prod
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ Eq.{u_2 + 1} (α := α) (∏ i : n, B ((g : (a : n) → n) i) i)
    (∏ i : n,
      (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i).coeff
        0)

Tactic:
Finset.prod_congr rfl ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
h :
  ∀ (x : n),
    Membership.mem (γ := Finset n) Finset.univ x →
      B ((g : (a : n) → n) x) x =
        (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) x) x).coeff
          0
⊢ Eq.{u_2 + 1} (α := α) (∏ i : n, B ((g : (a : n) → n) i) i)
    (∏ i : n,
      (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i).coeff
        0)

Tactic:
refine Finset.prod_congr rfl ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ (x : n),
    Membership.mem (γ := Finset n) Finset.univ x →
      B ((g : (a : n) → n) x) x =
        (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) x) x).coeff
          0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
rw :
  Eq.{u_2 + 1} (α := α)
    (∑ b : Equiv.Perm n,
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) b : ℤˣ)
            (∏ i : n,
              HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                (B.map (⇑C : (a : α) → α[X])) ((b : (a : n) → n) i) i)).coeff
        (Fintype.card n))
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A ((σ : (a : n) → n) i) i))
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])) +
            B.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n) =
    A.det

Tactic:
rw [det_apply, det_apply, finsetSum_coeff]

Premises used: Matrix.det_apply, Polynomial.finsetSum_coeff
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
⊢ Eq.{u_2 + 1} (α := α)
    (∑ b : Equiv.Perm n,
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) b : ℤˣ)
            (∏ i : n,
              HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                (B.map (⇑C : (a : α) → α[X])) ((b : (a : n) → n) i) i)).coeff
        (Fintype.card n))
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A ((σ : (a : n) → n) i) i))

Tactic:
Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
refine :
  ∀ (x : Equiv.Perm n),
    Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ x →
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
              (∏ i : n,
                HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                  (B.map (⇑C : (a : α) → α[X])) ((x : (a : n) → n) i) i)).coeff
          (Fintype.card n) =
        HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
          (∏ i : n, A ((x : (a : n) → n) i) i)
⊢ Eq.{u_2 + 1} (α := α)
    (∑ b : Equiv.Perm n,
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) b : ℤˣ)
            (∏ i : n,
              HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                (B.map (⇑C : (a : α) → α[X])) ((b : (a : n) → n) i) i)).coeff
        (Fintype.card n))
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A ((σ : (a : n) → n) i) i))

Tactic:
refine Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
simp :
  ∀ (x : Equiv.Perm n),
    (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
            (∏ i : n,
              HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                (B.map (⇑C : (a : α) → α[X])) ((x : (a : n) → n) i) i)).coeff
        (Fintype.card n) =
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
        (∏ i : n, A ((x : (a : n) → n) i) i)
⊢ ∀ (x : Equiv.Perm n),
    Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ x →
      (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
              (∏ i : n,
                HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
                  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
                  (B.map (⇑C : (a : α) → α[X])) ((x : (a : n) → n) i) i)).coeff
          (Fintype.card n) =
        HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
          (∏ i : n, A ((x : (a : n) → n) i) i)

Tactic:
simp only [Finset.mem_univ, forall_true_left]

Premises used: Finset.mem_univ, forall_true_left
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
          (∏ i : n,
            HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)).coeff
      (Fintype.card n) =
    HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
      (coeff
        (∏ i : n,
          HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
        (Fintype.card n))

Tactic:
coeff_smul (R := α) (sign g) _ _

Premises used: Equiv.Perm.sign, Polynomial.coeff_smul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
h :
  Eq.{u_2 + 1} (α := α) (∏ i : n, A ((g : (a : n) → n) i) i)
    (coeff
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
      (Fintype.card n))
⊢ (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
          (∏ i : n,
            HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)).coeff
      (Fintype.card n) =
    HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
      (∏ i : n, A ((g : (a : n) → n) i) i)

Tactic:
convert! coeff_smul (R := α) (sign g) _ _

Premises used: Equiv.Perm.sign, Polynomial.coeff_smul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
h :
  Eq.{u_2 + 1} (α := α) (∏ i : n, A ((g : (a : n) → n) i) i)
    (coeff
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
      (Fintype.card n * 1))
⊢ Eq.{u_2 + 1} (α := α) (∏ i : n, A ((g : (a : n) → n) i) i)
    (coeff
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
      (Fintype.card n))

Tactic:
rw [← mul_one (Fintype.card n)]

Premises used: Fintype.card, mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ Eq.{u_2 + 1} (α := α)
    (∏ i : n,
      (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i).coeff
        1)
    (coeff
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
      (Finset.card.{u_1} (α := n) Finset.univ * 1))

Tactic:
(coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm

Premises used: Eq.symm, Polynomial.coeff_prod_of_natDegree_le
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
h :
  ∀ (x : n),
    Membership.mem (γ := Finset n) Finset.univ x →
      A ((g : (a : n) → n) x) x =
        (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) x) x).coeff
          1
h₁ :
  ∀ (p : n),
    Membership.mem (γ := Finset n) Finset.univ p →
      (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) p) p).natDegree ≤
        1
⊢ Eq.{u_2 + 1} (α := α) (∏ i : n, A ((g : (a : n) → n) i) i)
    (coeff
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
      (Fintype.card n * 1))

Tactic:
convert! (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm

Premises used: Eq.symm, Polynomial.coeff_prod_of_natDegree_le
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
x : n
h : Membership.mem (γ := Finset n) Finset.univ x
⊢ A ((g : (a : n) → n) x) x =
    (HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) x) x).coeff
      1

Tactic:
simp [coeff_C]

Premises used: Polynomial.coeff_C
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
h : max (HAdd.hAdd (α := ℕ) 1 0) 0 ≤ 1
⊢ (HAdd.hAdd (β := α[X]) (HMul.hMul (α := α[X]) (β := α[X]) X ((C : (a : α) → α[X]) (A ((g : (a : n) → n) p) p) : α[X]))
        ((C : (a : α) → α[X]) (B ((g : (a : n) → n) p) p) : α[X])).natDegree ≤
    1

Tactic:
compute_degree
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
inl :
  Subsingleton α →
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 +
            A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
      1
inr :
  Nontrivial α →
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 +
            A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
      1
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
    1

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Subsingleton α
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
    1

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Nontrivial α
inr :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
            A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n)
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
    1

Tactic:
rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_det_X_add_C_card, Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Nontrivial α
inr :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n)
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
            A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n)

Tactic:
simp only [Matrix.map_one, C_eq_zero, map_one]

Premises used: Polynomial.C_eq_zero, Matrix.map_one, map_one
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Nontrivial α
inr :
  ∀
    (h :
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
              A.map (⇑C : (a : α) → α[X])).det.natDegree =
        Fintype.card n),
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
        (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 +
              A.map (⇑C : (a : α) → α[X])).det.natDegree =
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
        (Fintype.card n)
inr₁ :
  ∀
    (h :
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
              A.map (⇑C : (a : α) → α[X])).det.natDegree <
        Fintype.card n),
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
        (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 +
              A.map (⇑C : (a : α) → α[X])).det.natDegree =
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
        (Fintype.card n)
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n)

Tactic:
rcases (natDegree_det_X_add_C_le 1 A).eq_or_lt with h | h

Premises used: LE.le.eq_or_lt, Polynomial.natDegree_det_X_add_C_le, OfNat.ofNat