awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : NonAssocSemiring R
inst_2 : StarRing R
simp : ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ star (Perm.permMatrix R σ⁻¹ i j)) = Perm.permMatrix R σ⁻¹
⊢ (Perm.permMatrix R σ)ᴴ = Perm.permMatrix R σ⁻¹

Tactic:
simp only [conjTranspose, transpose_permMatrix, map]

Premises used: Matrix.transpose_permMatrix, Matrix.map, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : NonAssocSemiring R
inst_2 : StarRing R
⊢ ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ star (Perm.permMatrix R σ⁻¹ i j)) = Perm.permMatrix R σ⁻¹

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
inst_2 : CommRing R
rw : (Perm.permMatrix R σ * 1).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R) (det (n := n) (submatrix (m := n) 1 (⇑σ : (a : n) → n) id))
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₂ :
  HMul.hMul (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) (det.{u_2, u_1} (n := n) 1) =
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₃ :
  HMul.hMul (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) 1 =
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₄ rw₅ :
  Eq.{u_2 + 1} (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
⊢ (Perm.permMatrix R σ).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)

Tactic:
rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
    det_permute, det_one, mul_one]

Premises used: Matrix.det_permute, Equiv.Perm.permMatrix, PEquiv.toMatrix_toPEquiv_mul, Matrix.det_one, Matrix.mul_one, mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
inst_2 : AddCommMonoidWithOne R
⊢ Eq.{u_2 + 1} (α := R) (∑ i : n, (Perm.permMatrix R σ).diag i)
    (↑(Set.ncard (α := n) (Function.fixedPoints (⇑σ : (a : n) → n))) : R)

Tactic:
simp [toPEquiv_apply, ← Set.ncard_coe_finset, Function.fixedPoints, Function.IsFixedPt]

Premises used: Equiv.toPEquiv_apply, Function.fixedPoints, Function.IsFixedPt, Set.ncard_coe_finset
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
v : n → R
inst_2 : CommRing R
h : ∀ (j : n), (Perm.permMatrix R σ *ᵥ v) j = (v ∘ (⇑σ : (a : n) → n)) j
⊢ Perm.permMatrix R σ *ᵥ v = v ∘ (⇑σ : (a : n) → n)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
v : n → R
inst_2 : CommRing R
j : n
⊢ (Perm.permMatrix R σ *ᵥ v) j = (v ∘ (⇑σ : (a : n) → n)) j

Tactic:
simp [mulVec_eq_sum, Pi.single, Function.update, Equiv.eq_symm_apply]

Premises used: Function.update, Pi.single, Matrix.mulVec_eq_sum, Equiv.eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
v : n → R
inst_2 : CommRing R
h : ∀ (j : n), (v ᵥ* Perm.permMatrix R σ) j = (v ∘ (⇑(Equiv.symm σ) : (a : n) → n)) j
⊢ v ᵥ* Perm.permMatrix R σ = v ∘ (⇑(Equiv.symm σ) : (a : n) → n)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
v : n → R
inst_2 : CommRing R
j : n
⊢ (v ᵥ* Perm.permMatrix R σ) j = (v ∘ (⇑(Equiv.symm σ) : (a : n) → n)) j

Tactic:
simp [vecMul_eq_sum, Pi.single, Function.update, ← Equiv.symm_apply_eq σ]

Premises used: Function.update, Equiv.symm_apply_eq, Matrix.vecMul_eq_sum, Pi.single
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ τ : Perm n
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
rw : (toPEquiv (σ * τ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
rw₁ : (Equiv.trans τ σ).toPEquiv.toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
rw₂ : ((toPEquiv τ).trans (toPEquiv σ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
rw₃ rw₄ :
  HMul.hMul (α := Matrix n n R) (toPEquiv τ).toMatrix (toPEquiv σ).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
⊢ Perm.permMatrix R (σ * τ) = Perm.permMatrix R τ * Perm.permMatrix R σ

Tactic:
rw [Perm.permMatrix, Perm.mul_def, toPEquiv_trans, PEquiv.toMatrix_trans]

Premises used: Equiv.Perm.permMatrix, Equiv.Perm.mul_def, Equiv.toPEquiv_trans, PEquiv.toMatrix_trans
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ_1 τ_1 : Perm n
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
σ τ : Perm n
rw : Perm.permMatrix R (τ⁻¹ * σ⁻¹) = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
rw₁ rw₂ : Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
⊢ Perm.permMatrix R (σ * τ)⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹

Tactic:
rw [_root_.mul_inv_rev, permMatrix_mul]

Premises used: Matrix.permMatrix_mul, mul_inv_rev
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
𝕜 : Type u_3
inst_2 : RCLike 𝕜
⊢ LE.le (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
𝕜 : Type u_3
inst_2 : RCLike 𝕜
⊢ ∀ (x : EuclideanSpace 𝕜 n),
    norm (E := EuclideanSpace 𝕜 n)
        ((((LinearEquiv.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯) toEuclideanLin
                      LinearMap.toContinuousLinearMap :
                    (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                  (Perm.permMatrix 𝕜 σ) :
                EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
              (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n)
            x :
          EuclideanSpace 𝕜 n) ≤
      1 * ‖x‖

Tactic:
simp [EuclideanSpace.norm_eq, toLpLin_apply, permMatrix_mulVec,
      σ.sum_comp _ (fun i ↦ ‖_‖ ^ 2)]

Premises used: Norm.norm, EuclideanSpace.norm_eq, HPow.hPow, Matrix.permMatrix_mulVec, OfNat.ofNat, Matrix.toLpLin_apply, Equiv.Perm.sum_comp
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
𝕜 : Type u_3
inst_2 : RCLike 𝕜
inst_3 : Nonempty n
inhabit : ∀ (inhabited_h : Inhabited n), 1 ≤ ‖Perm.permMatrix 𝕜 σ‖
⊢ 1 ≤ ‖Perm.permMatrix 𝕜 σ‖

Tactic:
inhabit n
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
𝕜 : Type u_3
inst_2 : RCLike 𝕜
inst_3 : Nonempty n
inhabited_h : Inhabited n
⊢ 1 ≤ ‖Perm.permMatrix 𝕜 σ‖

Tactic:
simpa [EuclideanSpace.norm_eq, permMatrix_mulVec, ← Equiv.eq_symm_apply σ, apply_ite] using
      (σ.permMatrix 𝕜).l2_opNorm_mulVec (WithLp.toLp _ (Pi.single default 1))

Premises used: Inhabited.default, Matrix.l2_opNorm_mulVec, Equiv.Perm.permMatrix, WithLp.toLp, apply_ite, Pi.single, EuclideanSpace.norm_eq, Matrix.permMatrix_mulVec, OfNat.ofNat, Equiv.eq_symm_apply
-- 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 :
  natDegree.{u_2} (R := α)
      (∑ σ : Equiv.Perm n,
        HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
          (∏ 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])) ((σ : (a : n) → n) i) i)) ≤
    Fintype.card n
⊢ (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.natDegree ≤
    Fintype.card n

Tactic:
rw [det_apply]

Premises used: Matrix.det_apply
-- 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 α
⊢ natDegree.{u_2} (R := α)
      (∑ σ : Equiv.Perm n,
        HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
          (∏ 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])) ((σ : (a : n) → n) i) i)) ≤
    Fintype.card n

Tactic:
(natDegree_sum_le _ _).trans ?_

Premises used: Polynomial.natDegree_sum_le, LE.le.trans
-- 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 :
  Finset.fold.{u_1, 0} (α := Equiv.Perm n) max 0
      (Function.comp.{u_1 + 1, u_2 + 1, 1} (β := α[X]) natDegree fun (σ : Equiv.Perm n) ↦
        HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
          (∏ 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])) ((σ : (a : n) → n) i) i))
      Finset.univ ≤
    Fintype.card n
⊢ natDegree.{u_2} (R := α)
      (∑ σ : Equiv.Perm n,
        HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
          (∏ 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])) ((σ : (a : n) → n) i) i)) ≤
    Fintype.card n

Tactic:
refine (natDegree_sum_le _ _).trans ?_

Premises used: Polynomial.natDegree_sum_le, LE.le.trans
-- 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 α
⊢ Finset.fold.{u_1, 0} (α := Equiv.Perm n) max 0
      (Function.comp.{u_1 + 1, u_2 + 1, 1} (β := α[X]) natDegree fun (σ : Equiv.Perm n) ↦
        HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
          (∏ 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])) ((σ : (a : n) → n) i) i))
      Finset.univ ≤
    Fintype.card n

Tactic:
Multiset.max_le_of_forall_le _ _ ?_

Premises used: Finset.fold, Multiset.max_le_of_forall_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 α
refine :
  ∀
    x ∈
      Multiset.map.{0, u_1} (α := Equiv.Perm n)
        (Function.comp.{u_1 + 1, u_2 + 1, 1} (β := α[X]) natDegree fun (σ : Equiv.Perm n) ↦
          HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
            (∏ 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])) ((σ : (a : n) → n) i) i))
        (Finset.val Finset.univ),
    x ≤ Fintype.card n
⊢ Finset.fold.{u_1, 0} (α := Equiv.Perm n) max 0
      (Function.comp.{u_1 + 1, u_2 + 1, 1} (β := α[X]) natDegree fun (σ : Equiv.Perm n) ↦
        HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
          (∏ 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])) ((σ : (a : n) → n) i) i))
      Finset.univ ≤
    Fintype.card n

Tactic:
refine Multiset.max_le_of_forall_le _ _ ?_

Premises used: Multiset.max_le_of_forall_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 α
simp :
  ∀ (a : Equiv.Perm n),
    (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) a : ℤˣ)
          (∏ 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])) ((a : (a : n) → n) i) i)).natDegree ≤
      Fintype.card n
⊢ ∀
    x ∈
      Multiset.map.{0, u_1} (α := Equiv.Perm n)
        (Function.comp.{u_1 + 1, u_2 + 1, 1} (β := α[X]) natDegree fun (σ : Equiv.Perm n) ↦
          HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
            (∏ 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])) ((σ : (a : n) → n) i) i))
        (Finset.val Finset.univ),
    x ≤ Fintype.card n

Tactic:
simp only [forall_apply_eq_imp_iff, true_and, Function.comp_apply,
    Multiset.mem_map, exists_imp, Finset.mem_univ_val]

Premises used: Multiset.mem_map, Finset.mem_univ_val, Function.comp_apply, exists_imp, forall_apply_eq_imp_iff, true_and
-- 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
inl :
  ∀ (sg : Eq (α := ℤˣ) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
    (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)).natDegree ≤
      natDegree.{u_2} (R := α)
        (∏ 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)
inr :
  ∀ (sg : Eq (α := ℤˣ) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)),
    (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)).natDegree ≤
      natDegree.{u_2} (R := α)
        (∏ 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)
⊢ (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)).natDegree ≤
    natDegree.{u_2} (R := α)
      (∏ 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)

Tactic:
rcases Int.units_eq_one_or (sign g) with sg | sg

Premises used: Equiv.Perm.sign, Int.units_eq_one_or, 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
sg : Eq (α := ℤˣ) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
inl :
  (HSMul.hSMul (α := ℤˣ) (β := α[X]) 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)).natDegree ≤
    natDegree.{u_2} (R := α)
      (∏ 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)
inl₁ inl₂ :
  natDegree.{u_2} (R := α)
      (∏ 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) ≤
    natDegree.{u_2} (R := α)
      (∏ 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)
⊢ (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)).natDegree ≤
    natDegree.{u_2} (R := α)
      (∏ 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)

Tactic:
rw [sg, one_smul]

Premises used: one_smul
-- 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
⊢ natDegree.{u_2} (R := α)
      (∏ 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) ≤
    ∑ 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).natDegree

Tactic:
(natDegree_prod_le (Finset.univ : Finset n) fun i : n =>
        (X • A.map C + B.map C : Matrix n n α[X]) (g i) i)

Premises used: Polynomial.C, Finset.univ, Polynomial.natDegree_prod_le, HAdd.hAdd, Matrix.map, HSMul.hSMul, Polynomial.X, 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
⊢ ∑ 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).natDegree ≤
    HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := n) Finset.univ) 1

Tactic:
(Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)

Premises used: Finset.sum_le_card_nsmul, OfNat.ofNat
-- 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 (β := ℕ) (Finset.card.{u_1} (α := n) Finset.univ) 1 ≤ Fintype.card n

Tactic:
simp [mul_one, Finset.card_univ]

Premises used: Finset.card_univ, 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
natDegree :
  ∀ (i : n),
    Membership.mem (γ := Finset n) Finset.univ i →
      (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).natDegree ≤
        1
⊢ (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)).natDegree ≤
    Fintype.card n

Tactic:
calc
    natDegree (sign g • ∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) ≤
        natDegree (∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) := by
      rcases Int.units_eq_one_or (sign g) with sg | sg
      · rw [sg, one_smul]
      · rw [sg, Units.neg_smul, one_smul, natDegree_neg]
    _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C : Matrix n n α[X]) (g i) i) :=
      (natDegree_prod_le (Finset.univ : Finset n) fun i : n =>
        (X • A.map C + B.map C : Matrix n n α[X]) (g i) i)
    _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)
    _ ≤ Fintype.card n := by simp [mul_one, Finset.card_univ]

Premises used: Polynomial.C, Finset.univ, Equiv.Perm.sign, Polynomial.natDegree_prod_le, Fintype.card, Finset.prod, Finset.sum_le_card_nsmul, HAdd.hAdd, Matrix.map, Finset.card, HSMul.hSMul, Polynomial.natDegree, OfNat.ofNat, Polynomial.X, 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
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
a : max (HAdd.hAdd (α := ℕ) 1 0) 0 ≤ 1
⊢ (HAdd.hAdd (β := α[X]) (HMul.hMul (α := α[X]) (β := α[X]) X ((C : (a : α) → α[X]) (A ((g : (a : n) → n) i) i) : α[X]))
        ((C : (a : α) → α[X]) (B ((g : (a : n) → n) i) i) : α[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 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
        0)
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, B ((σ : (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
      0 =
    B.det

Tactic:
rw [det_apply, finsetSum_coeff, det_apply]

Premises used: Matrix.det_apply, Polynomial.finsetSum_coeff