awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
this : Eq (α := MvPolynomial (n × n) ℤ) (Polynomial.coeff (univ ℤ n) (Fintype.card n)) 1
rw :
  Eq (α := MvPolynomial.{u_3, u_1} (n × n) R)
    (Polynomial.coeff (Polynomial.map (R := MvPolynomial (n × n) ℤ) (MvPolynomial.map (Int.castRingHom R)) (univ ℤ n))
      (Fintype.card n))
    1
rw₁ :
  Eq (α := MvPolynomial.{u_3, u_1} (n × n) R)
    ((MvPolynomial.map (Int.castRingHom R) : (a : MvPolynomial (n × n) ℤ) → MvPolynomial (n × n) R)
        (Polynomial.coeff (univ ℤ n) (Fintype.card n)) :
      MvPolynomial.{u_3, u_1} (n × n) R)
    (1 : MvPolynomial.{u_3, u_1} (n × n) R)
rw₂ :
  Eq (α := MvPolynomial.{u_3, u_1} (n × n) R)
    ((MvPolynomial.map (Int.castRingHom R) : (a : MvPolynomial (n × n) ℤ) → MvPolynomial (n × n) R) 1) 1
rw₃ rw₄ : Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) 1 1
⊢ Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) (Polynomial.coeff (univ R n) (Fintype.card n)) 1

Tactic:
rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]

Premises used: Matrix.charpoly.univ_map_map, Polynomial.coeff_map, map_one, Int.castRingHom
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
suffices : Eq (α := MvPolynomial (n × n) ℤ) (Polynomial.coeff (univ ℤ n) (Fintype.card n)) 1
⊢ Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) (Polynomial.coeff (univ R n) (Fintype.card n)) 1

Tactic:
suffices Polynomial.coeff (univ ℤ n) (Fintype.card n) = 1 by
    rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
rw :
  Eq (α := MvPolynomial (n × n) ℤ)
    (Polynomial.coeff (univ ℤ n) (Polynomial.natDegree (R := MvPolynomial (n × n) ℤ) (univ ℤ n))) 1
⊢ Eq (α := MvPolynomial (n × n) ℤ) (Polynomial.coeff (univ ℤ n) (Fintype.card n)) 1

Tactic:
rw [← univ_natDegree ℤ n]

Premises used: Int, Matrix.charpoly.univ_natDegree
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := MvPolynomial (n × n) ℤ)
    (Polynomial.coeff (univ ℤ n) (Polynomial.natDegree (R := MvPolynomial (n × n) ℤ) (univ ℤ n))) 1

Tactic:
(univ_monic ℤ n).leadingCoeff

Premises used: Matrix.charpoly.univ_monic, Polynomial.leadingCoeff, Int, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := MvPolynomial (n × n) ℤ)
    (Polynomial.coeff (univ ℤ n) (Polynomial.natDegree (R := MvPolynomial (n × n) ℤ) (univ ℤ n))) 1

Tactic:
exact (univ_monic ℤ n).leadingCoeff

Premises used: Matrix.charpoly.univ_monic, Int, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)

Tactic:
simp only [zero_add, Finset.sum_const, smul_eq_mul, mul_one, Fintype.card]

Premises used: Fintype.card, zero_add, smul_eq_mul, mul_one, Finset.sum_const
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)

Tactic:
have aux : Fintype.card n = 0 + ∑ i : n, 1 := by
    simp only [zero_add, Finset.sum_const, smul_eq_mul, mul_one, Fintype.card]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
simp :
  IsHomogeneous.{u_3, u_1} (σ := Option (n × n)) (R := R)
    (∑ x : Equiv.Perm n,
      HMul.hMul (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) :
          MvPolynomial (Option (n × n)) R)
        (∏ x_1 : n,
          HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            ((Polynomial.aevalTower (rename some) (X none) :
                  (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
                (if (x : (a : n) → n) x_1 = x_1 then Polynomial.X else 0) :
              MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            (X (some ((x : (a : n) → n) x_1, x_1)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)))
    (HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1))
⊢ IsHomogeneous.{u_3, u_1} (σ := Option (n × n)) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R (n × n)) :
        (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
      (univ R n))
    (Fintype.card n)

Tactic:
simp only [aux, univ, charpoly, charmatrix, scalar_apply, RingHom.mapMatrix_apply, det_apply',
    sub_apply, map_apply, of_apply, map_sum, map_mul, map_intCast, map_prod, map_sub,
    optionEquivLeft_symm_apply, Polynomial.aevalTower_C, rename_X, diagonal, mvPolynomialX]

Premises used: RingHom.mapMatrix_apply, map_sub, Matrix.charpoly.univ, Matrix.sub_apply, Matrix.map_apply, Polynomial.aevalTower_C, Matrix.charmatrix, map_intCast, Matrix.of_apply, map_sum, map_prod, map_mul, MvPolynomial.optionEquivLeft_symm_apply, MvPolynomial.rename_X, Matrix.scalar_apply, Matrix.mvPolynomialX, Matrix.det_apply', Matrix.diagonal, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
h :
  ∀ (i : Equiv.Perm n),
    Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ i →
      (HMul.hMul (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) i) : ℤ) :
              MvPolynomial (Option (n × n)) R)
            (∏ x : n,
              HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β :=
                MvPolynomial.{u_3, u_1} (Option (n × n)) R)
                ((Polynomial.aevalTower (rename some) (X none) :
                      (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
                    (if (i : (a : n) → n) x = x then Polynomial.X else 0) :
                  MvPolynomial.{u_3, u_1} (Option (n × n)) R)
                (X (some ((i : (a : n) → n) x, x)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R))).IsHomogeneous
        (HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1))
⊢ IsHomogeneous.{u_3, u_1} (σ := Option (n × n)) (R := R)
    (∑ x : Equiv.Perm n,
      HMul.hMul (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) :
          MvPolynomial (Option (n × n)) R)
        (∏ x_1 : n,
          HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            ((Polynomial.aevalTower (rename some) (X none) :
                  (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
                (if (x : (a : n) → n) x_1 = x_1 then Polynomial.X else 0) :
              MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            (X (some ((x : (a : n) → n) x_1, x_1)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)))
    (HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1))

Tactic:
apply IsHomogeneous.sum

Premises used: MvPolynomial.IsHomogeneous.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
i : Equiv.Perm n
h :
  IsHomogeneous.{u_3, u_1} (σ := Option (n × n)) (R := R)
    (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) i) : ℤ) : MvPolynomial (Option (n × n)) R) 0
h₁ :
  IsHomogeneous.{u_3, u_1} (σ := Option (n × n)) (R := R)
    (∏ x : n,
      HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        ((Polynomial.aevalTower (rename some) (X none) :
              (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
            (if (i : (a : n) → n) x = x then Polynomial.X else 0) :
          MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (X (some ((i : (a : n) → n) x, x)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R))
    (∑ i : n, 1)
⊢ (HMul.hMul (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) i) : ℤ) :
          MvPolynomial (Option (n × n)) R)
        (∏ x : n,
          HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            ((Polynomial.aevalTower (rename some) (X none) :
                  (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
                (if (i : (a : n) → n) x = x then Polynomial.X else 0) :
              MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            (X (some ((i : (a : n) → n) x, x)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R))).IsHomogeneous
    (HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1))

Tactic:
apply IsHomogeneous.mul

Premises used: MvPolynomial.IsHomogeneous.mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
i : Equiv.Perm n
⊢ IsHomogeneous.{u_3, u_1} (σ := Option (n × n)) (R := R)
    (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) i) : ℤ) : MvPolynomial (Option (n × n)) R) 0

Tactic:
apply isHomogeneous_C

Premises used: MvPolynomial.isHomogeneous_C
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
i : Equiv.Perm n
h :
  ∀ (i_1 : n),
    Membership.mem (γ := Finset n) Finset.univ i_1 →
      (HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            ((Polynomial.aevalTower (rename some) (X none) :
                  (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
                (if (i : (a : n) → n) i_1 = i_1 then Polynomial.X else 0) :
              MvPolynomial.{u_3, u_1} (Option (n × n)) R)
            (X (some ((i : (a : n) → n) i_1, i_1)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)).IsHomogeneous
        1
⊢ IsHomogeneous.{u_3, u_1} (σ := Option (n × n)) (R := R)
    (∏ x : n,
      HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        ((Polynomial.aevalTower (rename some) (X none) :
              (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
            (if (i : (a : n) → n) x = x then Polynomial.X else 0) :
          MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (X (some ((i : (a : n) → n) x, x)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R))
    (∑ i : n, 1)

Tactic:
apply IsHomogeneous.prod

Premises used: MvPolynomial.IsHomogeneous.prod
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
i : Equiv.Perm n
j : n
pos :
  ∀ (h : (i : (a : n) → n) j = j),
    (HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
          ((Polynomial.aevalTower (rename some) (X none) :
                (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
              (if (i : (a : n) → n) j = j then Polynomial.X else 0) :
            MvPolynomial.{u_3, u_1} (Option (n × n)) R)
          (X (some ((i : (a : n) → n) j, j)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)).IsHomogeneous
      1
neg :
  ∀ (h : ¬(i : (a : n) → n) j = j),
    (HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
          ((Polynomial.aevalTower (rename some) (X none) :
                (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
              (if (i : (a : n) → n) j = j then Polynomial.X else 0) :
            MvPolynomial.{u_3, u_1} (Option (n × n)) R)
          (X (some ((i : (a : n) → n) j, j)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)).IsHomogeneous
      1
⊢ (HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        ((Polynomial.aevalTower (rename some) (X none) :
              (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
            (if (i : (a : n) → n) j = j then Polynomial.X else 0) :
          MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (X (some ((i : (a : n) → n) j, j)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)).IsHomogeneous
    1

Tactic:
by_cases h : i j = j

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
i : Equiv.Perm n
j : n
h : (i : (a : n) → n) j = j
⊢ (HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        ((Polynomial.aevalTower (rename some) (X none) :
              (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
            (if (i : (a : n) → n) j = j then Polynomial.X else 0) :
          MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (X (some ((i : (a : n) → n) j, j)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)).IsHomogeneous
    1

Tactic:
simp only [h, ↓reduceIte, Polynomial.aevalTower_X, IsHomogeneous.sub, isHomogeneous_X]

Premises used: Polynomial.aevalTower_X, MvPolynomial.IsHomogeneous.sub, MvPolynomial.isHomogeneous_X, reduceIte
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
aux : Fintype.card n = HAdd.hAdd (α := ℕ) 0 (∑ i : n, 1)
i : Equiv.Perm n
j : n
h : ¬(i : (a : n) → n) j = j
⊢ (HSub.hSub (α := MvPolynomial.{u_3, u_1} (Option (n × n)) R) (β := MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        ((Polynomial.aevalTower (rename some) (X none) :
              (a : Polynomial (MvPolynomial (n × n) R)) → MvPolynomial (Option (n × n)) R)
            (if (i : (a : n) → n) j = j then Polynomial.X else 0) :
          MvPolynomial.{u_3, u_1} (Option (n × n)) R)
        (X (some ((i : (a : n) → n) j, j)) : MvPolynomial.{u_3, u_1} (Option (n × n)) R)).IsHomogeneous
    1

Tactic:
simp only [h, ↓reduceIte, map_zero, zero_sub, (isHomogeneous_X _ _).neg]

Premises used: map_zero, MvPolynomial.isHomogeneous_X, reduceIte, MvPolynomial.IsHomogeneous.neg, zero_sub
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
i j : ℕ
h : i + j = Fintype.card n
⊢ MvPolynomial.IsHomogeneous (Polynomial.coeff (univ R n) i) j

Tactic:
(optionEquivLeft_symm_univ_isHomogeneous R n).coeff_isHomogeneous_of_optionEquivLeft_symm _ _ h

Premises used: Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : Sub n
v : n → α
i j : n
⊢ circulant v i j = v (i - j)

Tactic:
rfl

Premises used: Matrix.circulant, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
i : n
⊢ circulant v i 0 = v i

Tactic:
congr_arg v (sub_zero _)

Premises used: sub_zero, congr_arg, Matrix.circulant
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
h₁ : ∀ (k : n), v k = w k
⊢ v = w

Tactic:
ext k
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
h₁ : circulant v k 0 = w k
h₂ : circulant v k 0 = circulant w k 0
h₃ h₄ : circulant w k 0 = circulant w k 0
⊢ v k = w k

Tactic:
rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]

Premises used: Matrix.circulant_col_zero_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
⊢ Injective (β := Matrix (Fin 0) (Fin 0) α) fun (v : Fin 0 → α) ↦ circulant v

Tactic:
simp [Injective]

Premises used: Function.Injective
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v w : n → α
⊢ circulant v = circulant w ↔ v = w

Tactic:
circulant_injective.eq_iff

Premises used: Function.Injective.eq_iff, Matrix.circulant_injective
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : ℕ
v w : Fin n → α
⊢ circulant v = circulant w ↔ v = w

Tactic:
(Fin.circulant_injective n).eq_iff

Premises used: Function.Injective.eq_iff, Matrix.Fin.circulant_injective
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
a : ∀ (i j : n), (circulant v)ᵀ i j = circulant (fun (i : n) ↦ v (-i)) i j
⊢ (circulant v)ᵀ = circulant fun (i : n) ↦ v (-i)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
i j : n
⊢ (circulant v)ᵀ i j = circulant (fun (i : n) ↦ v (-i)) i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : Star α
inst_1 : SubtractionMonoid n
v : n → α
a : ∀ (i j : n), (circulant v)ᴴ i j = circulant (star fun (i : n) ↦ v (-i)) i j
⊢ (circulant v)ᴴ = circulant (star fun (i : n) ↦ v (-i))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : Star α
inst_1 : SubtractionMonoid n
v : n → α
i j : n
⊢ (circulant v)ᴴ i j = circulant (star fun (i : n) ↦ v (-i)) i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
⊢ ∀ (v : Fin 0 → α), (circulant v)ᵀ = circulant fun (i : Fin 0) ↦ v (-i)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
inst : Star α
⊢ ∀ (v : Fin 0 → α), (circulant v)ᴴ = circulant (star fun (i : Fin 0) ↦ v (-i))

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
inst : Sub n
v : n → α
f : α → β
⊢ (circulant v).map f = circulant fun (i : n) ↦ f (v i)

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : Neg α
inst_1 : Sub n
v : n → α
⊢ circulant (-v) = -circulant v

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_5
n : Type u_6
inst : Zero α
inst_1 : Sub n
⊢ Eq (α := Matrix n n α) (circulant 0) 0

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : Add α
inst_1 : Sub n
v w : n → α
⊢ circulant (v + w) = circulant v + circulant w

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : Sub α
inst_1 : Sub n
v w : n → α
⊢ circulant (v - w) = circulant v - circulant w

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : AddGroup n
v w : n → α
a : ∀ (i j : n), (circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j
⊢ circulant v * circulant w = circulant (circulant v *ᵥ w)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : AddGroup n
v w : n → α
i j : n
a : Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, v (i - j - x) * w x)
⊢ (circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j

Tactic:
simp only [mul_apply, mulVec, circulant_apply, dotProduct]

Premises used: dotProduct, Matrix.circulant_apply, Matrix.mul_apply, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : AddGroup n
v w : n → α
i j : n
⊢ Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, v (i - j - x) * w x)

Tactic:
Fintype.sum_equiv (Equiv.subRight j) _ _ ?_

Premises used: Equiv.subRight, Fintype.sum_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : AddGroup n
v w : n → α
i j : n
a :
  ∀ (x : n),
    v (i - x) * w (x - j) =
      v (HSub.hSub (β := n) (i - j) ((Equiv.subRight j : (a : n) → n) x : n)) * w ((Equiv.subRight j : (a : n) → n) x)
⊢ Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, v (i - j - x) * w x)

Tactic:
refine Fintype.sum_equiv (Equiv.subRight j) _ _ ?_

Premises used: Equiv.subRight, Fintype.sum_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) =
    v (HSub.hSub (β := n) (i - j) ((Equiv.subRight j : (a : n) → n) x : n)) * w ((Equiv.subRight j : (a : n) → n) x)

Tactic:
simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]

Premises used: sub_sub_sub_cancel_right, Equiv.subRight_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant (circulant v *ᵥ w)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
a : ∀ (i j : n), (circulant v * circulant w) i j = (circulant w * circulant v) i j
⊢ circulant v * circulant w = circulant w * circulant v

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
i j : n
a : Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, w (i - x) * v (x - j))
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j

Tactic:
simp only [mul_apply, circulant_apply]

Premises used: Matrix.circulant_apply, Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
i j : n
⊢ Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, w (i - x) * v (x - j))

Tactic:
Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ ?_

Premises used: Equiv.addRight, Equiv.subLeft, Equiv.trans, Fintype.sum_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
i j : n
a :
  ∀ (x : n),
    v (i - x) * w (x - j) =
      w (HSub.hSub (β := n) i (((Equiv.subLeft i).trans (Equiv.addRight j) : (a : n) → n) x : n)) *
        v (HSub.hSub (α := n) (((Equiv.subLeft i).trans (Equiv.addRight j) : (a : n) → n) x : n) j)
⊢ Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, w (i - x) * v (x - j))

Tactic:
refine Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ ?_

Premises used: Equiv.addRight, Equiv.subLeft, Equiv.trans, Fintype.sum_equiv