awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
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 τ⁻¹
⊢ Perm.permMatrix R (σ * τ)⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
have rw₁ : Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
Tactic: rw [_root_.mul_inv_rev, permMatrix_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
𝕜 : Type u_3
inst_2 : RCLike 𝕜
inst_3 : Nonempty n
⊢ 1 ≤ ‖Perm.permMatrix 𝕜 σ‖
have inhabit : ∀ (inhabited_h : Inhabited n), 1 ≤ ‖Perm.permMatrix 𝕜 σ‖
Tactic: inhabit n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n 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
have 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
Tactic: rw [det_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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
have 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
Tactic: refine (natDegree_sum_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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
have 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
Tactic: refine Multiset.max_le_of_forall_le _ _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n 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
have 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
Tactic: simp only [forall_apply_eq_imp_iff, true_and, Function.comp_apply,
    Multiset.mem_map, exists_imp, Finset.mem_univ_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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)).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)
have 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)
Tactic: rcases Int.units_eq_one_or (sign g) with sg | sg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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)
⊢ (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)
have 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)
Tactic: rcases Int.units_eq_one_or (sign g) with sg | sg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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 : ℤˣ)
⊢ (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)
have 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)
Tactic: rw [sg, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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)
⊢ (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)
have 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)
Tactic: rw [sg, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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 : ℤˣ)
⊢ (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)
have inr : (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)
Tactic: rw [sg, Units.neg_smul, one_smul, natDegree_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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 : ℤˣ)
inr :
  (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)
⊢ (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)
have inr₁ : (-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)
Tactic: rw [sg, Units.neg_smul, one_smul, natDegree_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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 : ℤˣ)
inr :
  (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)
inr₁ :
  (-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)
⊢ (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)
have inr₂ : 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)
Tactic: rw [sg, Units.neg_smul, one_smul, natDegree_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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)).natDegree ≤
    Fintype.card n
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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
⊢ (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
have a : max (HAdd.hAdd (α := ℕ) 1 0) 0 ≤ 1
Tactic: compute_degree
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n 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.coeff
      0 =
    B.det
have 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))
Tactic: rw [det_apply, finsetSum_coeff, det_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl ?_