/-- **Eckmann–Hilton.** If a set carries two binary operations `m₁`, `m₂` with units `e₁`, `e₂`
that satisfy the interchange law `(a ·₂ b) ·₁ (c ·₂ d) = (a ·₁ c) ·₂ (b ·₁ d)`, then the units
agree, the operations agree, and the operation is commutative. For `πₙ` with `n ≥ 2`,
concatenation of cubes in two different coordinate directions gives two such operations. -/
theorem eckmann_hilton {M : Type*} (m₁ m₂ : M → M → M) (e₁ e₂ : M)
(h₁l : ∀ a, m₁ e₁ a = a) (h₁r : ∀ a, m₁ a e₁ = a)
(h₂l : ∀ a, m₂ e₂ a = a) (h₂r : ∀ a, m₂ a e₂ = a)
(interchange : ∀ a b c d, m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
e₁ = e₂ ∧ (∀ a b, m₁ a b = m₂ a b) ∧ (∀ a b, m₁ a b = m₁ b a) := by
-- the units agree
have he : e₁ = e₂ :=
calc e₁ = m₁ e₁ e₁ := (h₁l e₁).symm
_ = m₁ (m₂ e₂ e₁) (m₂ e₁ e₂) := by rw [h₂l, h₂r]
_ = m₂ (m₁ e₂ e₁) (m₁ e₁ e₂) := interchange _ _ _ _
_ = m₂ e₂ e₂ := by rw [h₁r, h₁l]
_ = e₂ := h₂l e₂
-- the operations agree
have hm : ∀ a b, m₁ a b = m₂ a b := fun a b =>
calc m₁ a b = m₁ (m₂ a e₂) (m₂ e₂ b) := by rw [h₂r, h₂l]
_ = m₂ (m₁ a e₂) (m₁ e₂ b) := interchange _ _ _ _
_ = m₂ a b := by rw [← he, h₁r, h₁l]
refine ⟨he, hm, fun a b => ?_⟩
-- and the operation is commutative
calc m₁ a b = m₁ (m₂ e₂ a) (m₂ b e₂) := by rw [h₂l, h₂r]
_ = m₂ (m₁ e₂ b) (m₁ a e₂) := interchange _ _ _ _
_ = m₂ b a := by rw [← he, h₁l, h₁r]
_ = m₁ b a := (hm b a).symm