calc
  (a₁ + b₁, a₂ + b₂) ≃ _ := AA.substL AA.comm
  (b₁ + a₁, a₂ + b₂) ≃ _ := AA.substR AA.comm
  (b₁ + a₁, b₂ + a₂) ≃ _ := Rel.refl
case a
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁, a₂ + b₂) ≃ (b₁ + a₁, b₂ + a₂)
no goals