English
Four-way commutativity of sum: the nesting (α ⊕ β) ⊕ γ ⊕ δ is naturally equivalent to (α ⊕ γ) ⊕ β ⊕ δ.
Русский
Четырёхразовая коммутативность суммы: вложенная сумма (α ⊕ β) ⊕ γ ⊕ δ естественным образом эквивалентна (α ⊕ γ) ⊕ β ⊕ δ.
LaTeX
$$$$(\alpha \oplus \beta) \oplus \gamma \oplus \delta \simeq (\alpha \oplus \gamma) \oplus \beta \oplus \delta.$$$$
Lean4
/-- Four-way commutativity of `sum`. The name matches `add_add_add_comm`. -/
@[simps apply]
def sumSumSumComm (α β γ δ) : (α ⊕ β) ⊕ γ ⊕ δ ≃ (α ⊕ γ) ⊕ β ⊕ δ
where
toFun :=
(sumAssoc (α ⊕ γ) β δ) ∘
(Sum.map (sumAssoc α γ β).symm (@id δ)) ∘
(Sum.map (Sum.map (@id α) (sumComm β γ)) (@id δ)) ∘
(Sum.map (sumAssoc α β γ) (@id δ)) ∘ (sumAssoc (α ⊕ β) γ δ).symm
invFun :=
(sumAssoc (α ⊕ β) γ δ) ∘
(Sum.map (sumAssoc α β γ).symm (@id δ)) ∘
(Sum.map (Sum.map (@id α) (sumComm β γ).symm) (@id δ)) ∘
(Sum.map (sumAssoc α γ β) (@id δ)) ∘ (sumAssoc (α ⊕ γ) β δ).symm
left_inv x := by rcases x with ((a | b) | (c | d)) <;> simp
right_inv x := by rcases x with ((a | c) | (b | d)) <;> simp
