calc
  _ = b₁            := rfl
  _ ≃ -a + (a + b₁) := Rel.symm reduce
  _ ≃ -a + (a + b₂) := AA.substR ‹a + b₁ ≃ a + b₂›
  _ ≃ b₂            := reduce
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
reduce : ∀ {x y : ℤ}, -x + (x + y) ≃ y
⊢ b₁ ≃ b₂
no goals