awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)).coeff
      0 =
    HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
      (∏ i : n, B ((g : (a : n) → n) i) i)
have 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)
Tactic: convert! coeff_smul (R := α) (sign g) _ 0
-- 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
⊢ 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)
have 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)
Tactic: rw [coeff_zero_prod]
-- 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
⊢ 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)
have 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
Tactic: refine Finset.prod_congr rfl ?_
-- 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
      (Fintype.card n) =
    A.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
      (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: rw [det_apply, det_apply, finsetSum_coeff]
-- 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
        (Fintype.card n))
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A ((σ : (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
        (Fintype.card n) =
      HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x : ℤˣ)
        (∏ i : n, A ((x : (a : n) → n) i) i)
Tactic: refine Finset.sum_congr rfl ?_
-- 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 : 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)
have 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)
Tactic: simp only [Finset.mem_univ, forall_true_left]
-- 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)).coeff
      (Fintype.card n) =
    HSMul.hSMul (α := ℤˣ) (β := α) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
      (∏ i : n, A ((g : (a : n) → n) i) i)
have 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))
Tactic: convert! coeff_smul (R := α) (sign g) _ _
-- 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
⊢ 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))
have 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))
Tactic: rw [← mul_one (Fintype.card 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 α
g : Equiv.Perm n
⊢ 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))
have 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
Tactic: convert! (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
-- 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
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
⊢ 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))
have 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
Tactic: convert! (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
-- 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
p : n
⊢ (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
have h : 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 : Matrix n n α
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
    1
have 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
Tactic: cases subsingleton_or_nontrivial α
-- 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 : 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
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
    1
have 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
Tactic: cases subsingleton_or_nontrivial α
-- 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 : Matrix n n α
h : Nontrivial α
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.leadingCoeff =
    1
have 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)
Tactic: rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]
-- 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 : Matrix n n α
h : Nontrivial α
⊢ (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)
have 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)
Tactic: simp only [Matrix.map_one, C_eq_zero, map_one]
-- 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 : Matrix n n α
h : Nontrivial α
⊢ (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)
have 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)
Tactic: rcases (natDegree_det_X_add_C_le 1 A).eq_or_lt with h | h
-- 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 : 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)
⊢ (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)
have 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)
Tactic: rcases (natDegree_det_X_add_C_le 1 A).eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (hypothesis)
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
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)
have h₁ : (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
  Fintype.card n
Tactic: simp only [map_one, Matrix.map_one, C_eq_zero] at h
Cleared hypotheses: h
-- 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 : Matrix n n α
h_1 : Nontrivial α
h :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + 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)
have inr : (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
    (Fintype.card n)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (hypothesis)
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
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)
have 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.coeff
    (Fintype.card n) =
  0
Tactic: have H := coeff_eq_zero_of_natDegree_lt h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (hypothesis)
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
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
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.coeff
      (Fintype.card n) =
    0
⊢ (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)
have H₁ : Eq.{u_2 + 1} (α := α) (det.{u_2, u_1} (n := n) 1) 0
Tactic: rw [coeff_det_X_add_C_card] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
⊢ LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * diagonal d i j * xj)
have refine : ∀ i ∈ x.support,
  ∀ j ∈ x.support,
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j))
        ((x : (a : n) → R) j : R)
Tactic: refine Finsupp.sum_nonneg fun i _ ↦ Finsupp.sum_nonneg fun j _ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ (M.submatrix e e).PosSemidef
have refine : ∀ (x : m →₀ R),
  LE.le (α := R) 0 (x.sum fun (i : m) (xi : R) ↦ x.sum fun (j : m) (xj : R) ↦ star xi * M.submatrix e e i j * xj)
Tactic: refine ⟨hM.1.submatrix _, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
⊢ Mᵀ.PosSemidef
have this : ∀ (a b c : R'), a * b * c = c * b * a
Tactic: have (a b c : R') : a * b * c = c * b * a := by ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
⊢ Mᵀ.PosSemidef
have refine : ∀ (x : n →₀ R'), LE.le (α := R') 0 (x.sum fun (i : n) (xi : R') ↦ x.sum fun (j : n) (xj : R') ↦ star xi * Mᵀ i j * xj)
Tactic: refine ⟨hM.1.transpose, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ LE.le (α := R') 0 (x.sum fun (i : n) (xi : R') ↦ x.sum fun (j : n) (xj : R') ↦ star xi * Mᵀ i j * xj)
have rw : LE.le (α := R') 0 (x.sum fun (x' : n) (v' : R') ↦ x.sum fun (x : n) (v : R') ↦ star v * Mᵀ x x' * v')
Tactic: rw [Finsupp.sum_comm]