α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₁ → ∀ (z : α), z * x * y = z * y * x
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ prod l₁ = prod l₂
refine h.foldl_eq' ?_ _
case H
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Symmetric fun x y => ∀ (z : α), z * x * y = z * y * x

case H₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : α), x ∈ l₁ → ∀ (z : α), z * x * x = z * x * x

case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : α), z * x * y = z * y * x) l₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₁ → ∀ (z : α), z * x * y = z * y * x
apply Pairwise.forall_of_forall
case H₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : α), x ∈ l₁ → ∀ (z : α), z * x * x = z * x * x

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

case H₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : α), x ∈ l₁ → ∀ (z : α), z * x * x = z * x * x

case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : α), z * x * y = z * y * x) l₁
. intro x y h z
  exact (h z).symm
case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : α), z * x * y = z * y * x) l₁
case H₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : α), x ∈ l₁ → ∀ (z : α), z * x * x = z * x * x

case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : α), z * x * y = z * y * x) l₁
. intros; rfl
no goals
case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : α), z * x * y = z * y * x) l₁
. apply hc.imp
  intro a b h z
  rw [mul_assoc z, mul_assoc z, h]
case H
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
x y : α
h : ∀ (z : α), z * x * y = z * y * x
z : α
⊢ z * y * x = z * x * y
case H
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Symmetric fun x y => ∀ (z : α), z * x * y = z * y * x
intro x y h z
no goals
case H
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
x y : α
h : ∀ (z : α), z * x * y = z * y * x
z : α
⊢ z * y * x = z * x * y
exact (h z).symm
case H₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
x✝ : α
a✝ : x✝ ∈ l₁
z✝ : α
⊢ z✝ * x✝ * x✝ = z✝ * x✝ * x✝
case H₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : α), x ∈ l₁ → ∀ (z : α), z * x * x = z * x * x
intros
no goals
case H₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
x✝ : α
a✝ : x✝ ∈ l₁
z✝ : α
⊢ z✝ * x✝ * x✝ = z✝ * x✝ * x✝
rfl
case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ {a b : α}, Commute a b → ∀ (z : α), z * a * b = z * b * a
case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun x y => ∀ (z : α), z * x * y = z * y * x) l₁
apply hc.imp
case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
a b : α
h : Commute a b
z : α
⊢ z * a * b = z * b * a
case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ {a b : α}, Commute a b → ∀ (z : α), z * a * b = z * b * a
intro a b h z
no goals
case H₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
M : Monoid α
l₁ l₂ : List α
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
a b : α
h : Commute a b
z : α
⊢ z * a * b = z * b * a
rw [mul_assoc z, mul_assoc z, h]