-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
/-- If elements of a list commute with each other, then their product does not
depend on the order of elements. -/
@[to_additive "If elements of a list additively commute with each other, then their sum does not
depend on the order of elements."]
lemma Perm.prod_eq' (h : l₁ ~ l₂) (hc : l₁.Pairwise Commute) : l₁.prod = l₂.prod

Proof state:
case H₁
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
x✝ : M
a✝ : x✝ ∈ l₁
z✝ : M
⊢ x✝ * (x✝ * z✝) = x✝ * (x✝ * z✝)

Tactic:
rfl

Result:
no goals

Proof state:
case H
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Symmetric fun x y => ∀ (z : M), y * (x * z) = x * (y * z)

Tactic:
intro x y h z

Result:
case H
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
x y : M
h : ∀ (z : M), y * (x * z) = x * (y * z)
z : M
⊢ x * (y * z) = y * (x * z)

Proof state:
case H₂
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : M), y * (x * z) = x * (y * z)) l₁

Tactic:
apply hc.imp

Result:
case H₂
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ {a b : M}, Commute a b → ∀ (z : M), b * (a * z) = a * (b * z)

Proof state:
case H₂
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ {a b : M}, Commute a b → ∀ (z : M), b * (a * z) = a * (b * z)

Tactic:
intro a b h z

Result:
case H₂
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
a b : M
h : Commute a b
z : M
⊢ b * (a * z) = a * (b * z)

Proof state:
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z : M), y * (x * z) = x * (y * z)

Tactic:
apply Pairwise.forall_of_forall

Result:
case H
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Symmetric fun x y => ∀ (z : M), y * (x * z) = x * (y * z)

case H₁
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ x ∈ l₁, ∀ (z : M), x * (x * z) = x * (x * z)

case H₂
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : M), y * (x * z) = x * (y * z)) l₁

Proof state:
case H₁
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ x ∈ l₁, ∀ (z : M), x * (x * z) = x * (x * z)

Tactic:
intros

Result:
case H₁
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
x✝ : M
a✝ : x✝ ∈ l₁
z✝ : M
⊢ x✝ * (x✝ * z✝) = x✝ * (x✝ * z✝)

Proof state:
case H₂
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
a b : M
h : Commute a b
z : M
⊢ b * (a * z) = a * (b * z)

Tactic:
rw [← mul_assoc, ← mul_assoc, h]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ l₁.prod = l₂.prod

Tactic:
refine h.foldr_eq' ?_ _

Result:
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z : M), y * (x * z) = x * (y * z)

Proof state:
case H
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
x y : M
h : ∀ (z : M), y * (x * z) = x * (y * z)
z : M
⊢ x * (y * z) = y * (x * z)

Tactic:
exact (h z).symm

Result:
no goals