awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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
⊢ Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) (Polynomial.coeff (univ R n) (Fintype.card n)) 1
have 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)
Tactic: rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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)
⊢ Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) (Polynomial.coeff (univ R n) (Fintype.card n)) 1
have 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
Tactic: rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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
⊢ Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) (Polynomial.coeff (univ R n) (Fintype.card n)) 1
have rw₃ : Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) 1 1
Tactic: rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) (Polynomial.coeff (univ R n) (Fintype.card n)) 1
have suffices : Eq (α := MvPolynomial (n × n) ℤ) (Polynomial.coeff (univ ℤ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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) (Fintype.card n)) 1
have rw : Eq (α := MvPolynomial (n × n) ℤ)
  (Polynomial.coeff (univ ℤ n) (Polynomial.natDegree (R := MvPolynomial (n × n) ℤ) (univ ℤ n))) 1
Tactic: rw [← univ_natDegree ℤ n]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (hypothesis)
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ 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)
have aux : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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)
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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)
⊢ 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))
have 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))
Tactic: apply IsHomogeneous.sum
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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
⊢ (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))
have 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
Tactic: apply IsHomogeneous.mul
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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
⊢ (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))
have 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)
Tactic: apply IsHomogeneous.mul
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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)
    (∏ 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)
have 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
Tactic: apply IsHomogeneous.prod
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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
⊢ (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
have 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
Tactic: by_cases h : i j = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
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
⊢ (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
have 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
Tactic: by_cases h : i j = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
⊢ v = w
have h₁ : ∀ (k : n), v k = w k
Tactic: ext k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k
have h₁ : circulant v k 0 = w k
Tactic: rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
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
⊢ v k = w k
have h₂ : circulant v k 0 = circulant w k 0
Tactic: rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
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
⊢ v k = w k
have h₃ : circulant w k 0 = circulant w k 0
Tactic: rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
⊢ (circulant v)ᵀ = circulant fun (i : n) ↦ v (-i)
have a : ∀ (i j : n), (circulant v)ᵀ i j = circulant (fun (i : n) ↦ v (-i)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : Star α
inst_1 : SubtractionMonoid n
v : n → α
⊢ (circulant v)ᴴ = circulant (star fun (i : n) ↦ v (-i))
have a : ∀ (i j : n), (circulant v)ᴴ i j = circulant (star fun (i : n) ↦ v (-i)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : AddGroup n
v w : n → α
⊢ circulant v * circulant w = circulant (circulant v *ᵥ w)
have a : ∀ (i j : n), (circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
inst_2 : AddGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j
have a : Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, v (i - j - x) * w x)
Tactic: simp only [mul_apply, mulVec, circulant_apply, dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
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)
have 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)
Tactic: refine Fintype.sum_equiv (Equiv.subRight j) _ _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
⊢ circulant v * circulant w = circulant w * circulant v
have a : ∀ (i j : n), (circulant v * circulant w) i j = (circulant w * circulant v) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
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
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j
have a : Eq.{u_1 + 1} (α := α) (∑ x : n, v (i - x) * w (x - j)) (∑ x : n, w (i - x) * v (x - j))
Tactic: simp only [mul_apply, circulant_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
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))
have 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)
Tactic: refine Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
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 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)
have a : v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
Tactic: simp only [Equiv.trans_apply, Equiv.subLeft_apply, Equiv.coe_addRight, add_sub_cancel_right,
    mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
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 x : n
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
have a : x - j = i - (i - x + j)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_5
n : Type u_6
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq n
inst_3 : AddGroup n
⊢ Eq (α := Matrix n n α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 1)) 1
have a : ∀ (i j : n), Eq.{u_5 + 1} (α := α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 1) i j) (1 i j)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_5
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : AddGroup n
inst_3 : Fintype n
a : α
⊢ Eq (α := Matrix n n α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 a)) ((scalar n : (a : α) → Matrix n n α) a)
have a₁ : ∀ (i j : n),
  Eq.{u_1 + 1} (α := α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 a) i j : α)
    ((scalar n : (a : α) → Matrix n n α) a i j : α)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_5
inst : Zero α
inst_1 : One α
n : ℕ
⊢ Eq.{u_5 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) α)
    (circulant fun (i : Fin (n + 1)) ↦ if (↑i : ℕ) = 0 then 1 else 0) 1
have rw : Eq.{u_5 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) α)
  (circulant fun (i : Fin (n + 1)) ↦ if (↑i : ℕ) = 0 then 1 else 0)
  (circulant (Pi.single (M := fun (a : Fin (n + 1)) ↦ α) 0 1))
Tactic: rw [← circulant_single_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_5
inst : Zero α
inst_1 : One α
n : ℕ
⊢ Eq.{u_5 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) α)
    (circulant fun (i : Fin (n + 1)) ↦ if (↑i : ℕ) = 0 then 1 else 0)
    (circulant (Pi.single (M := fun (a : Fin (n + 1)) ↦ α) 0 1))
have e_v : ∀ (j : Fin (n + 1)),
  Eq.{u_5 + 1} (α := α) (if (↑j : ℕ) = 0 then 1 else 0 : α) (Pi.single (M := fun (a : Fin (n + 1)) ↦ α) 0 1 j : α)
Tactic: congr with j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
⊢ (circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
have rw : (circulant v)ᵀ = circulant v ↔ ∀ (i : n), v (-i) = v i
Tactic: rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
rw : (circulant v)ᵀ = circulant v ↔ ∀ (i : n), v (-i) = v i
⊢ (circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
have rw₁ : (circulant fun (i : n) ↦ v (-i)) = circulant v ↔ ∀ (i : n), v (-i) = v i
Tactic: rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
rw : (circulant v)ᵀ = circulant v ↔ ∀ (i : n), v (-i) = v i
rw₁ : (circulant fun (i : n) ↦ v (-i)) = circulant v ↔ ∀ (i : n), v (-i) = v i
⊢ (circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
have rw₂ : (fun (i : n) ↦ v (-i)) = v ↔ ∀ (i : n), v (-i) = v i
Tactic: rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]