-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem circulant_mul_comm [CommSemigroup α] [AddCommMonoid α] [Fintype n] [AddCommGroup n]
    (v w : n → α) : circulant v * circulant w = circulant w * circulant v

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∀ (x : n),
    v (i - x) * w (x - j) =
      w (i - ((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)

Tactic:
intro x

Result:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) =
    w (i - ((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))

Tactic:
congr 2

Result:
case a.e_a.e_a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)

Proof state:
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
⊢ circulant v * circulant w = circulant w * circulant v

Tactic:
ext i j

Result:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j

Tactic:
simp only [mul_apply, circulant_apply, mul_comm]

Result:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, w (i - x) * v (x - j)

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) =
    w (i - ((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)

Tactic:
simp only [Equiv.trans_apply, Equiv.subLeft_apply, Equiv.coe_addRight, add_sub_cancel_right,
  mul_comm]

Result:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∑ 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)) _ _ ?_

Result:
case a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∀ (x : n),
    v (i - x) * w (x - j) =
      w (i - ((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)

Proof state:
case a.e_a.e_a
α : Type u_1
n : Type u_3
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)

Tactic:
abel

Result:
no goals