match this with
| AA.OneOfThree.first (_ : sgn p ≃ 0) =>
  have : (0 : ℤ) < 1 := Integer.zero_lt_one
  have : (0 : ℤ) ≤ 1 := Integer.le_iff_lt_or_eqv.mpr (Or.inl this)
  have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ 0›) this
  exact this
| AA.OneOfThree.second (_ : sgn p ≃ 1) =>
  have : (1 : ℤ) ≤ 1 := Integer.le_refl
  have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ 1›) this
  exact this
| AA.OneOfThree.third (_ : sgn p ≃ -1) =>
  have : (-1 : ℤ) < 0 := Integer.neg_one_lt_zero
  have : (0 : ℤ) < 1 := Integer.zero_lt_one
  have : (-1 : ℤ) < 1 := Integer.lt_trans ‹(-1 : ℤ) < 0› ‹(0 : ℤ) < 1›
  have : (-1 : ℤ) ≤ 1 := Integer.le_iff_lt_or_eqv.mpr (Or.inl this)
  have : sgn p ≤ 1 := Integer.le_substL_eqv (Rel.symm ‹sgn p ≃ -1›) this
  exact this
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
⊢ sgn p ≤ 1
no goals