have : a ≤ b := match ‹a < b ∨ a ≃ b› with
| Or.inl (_ : a < b) =>
  have (And.intro (_ : a ≤ b) _) := lt_iff_le_neqv.mp ‹a < b›
  ‹a ≤ b›
| Or.inr (_ : a ≃ b) =>
  have : a ≤ a := le_refl
  have : a ≤ b := AA.substRFn ‹a ≃ b› ‹a ≤ a›
  ‹a ≤ b›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a < b ∨ a ≃ b
⊢ a ≤ b
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a < b ∨ a ≃ b
this : a ≤ b
⊢ a ≤ b