case mp
x y : EReal
⊢ x ≤ y →
    ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y

case mpr
x y : EReal
⊢ ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y →
    x ≤ y
x y : EReal
⊢ x ≤ y ↔
    ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
constructor
case mp
x y : EReal
h : x ≤ y
⊢ ↑sign x < ↑sign y ∨
    ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
      ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
        ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
case mp
x y : EReal
⊢ x ≤ y →
    ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
intro h
case mp
x y : EReal
h : x ≤ y
hs : ↑sign x = ↑sign y
⊢ ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
      ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
case mp
x y : EReal
h : x ≤ y
⊢ ↑sign x < ↑sign y ∨
    ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
      ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
        ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)
case mp
x y : EReal
h : ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
⊢ ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
      ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
case mp
x y : EReal
h : x ≤ y
hs : ↑sign x = ↑sign y
⊢ ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
      ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
case mp.zero
x y : EReal
h : ↑SignType.zero * ↑(EReal.abs x) ≤ ↑SignType.zero * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.zero
⊢ SignType.zero = SignType.neg ∧ SignType.zero = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.zero = SignType.zero ∧ SignType.zero = SignType.zero ∨
      SignType.zero = SignType.pos ∧ SignType.zero = SignType.pos ∧ EReal.abs x ≤ EReal.abs y

case mp.neg
x y : EReal
h : ↑SignType.neg * ↑(EReal.abs x) ≤ ↑SignType.neg * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.neg
⊢ SignType.neg = SignType.neg ∧ SignType.neg = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.neg = SignType.zero ∧ SignType.neg = SignType.zero ∨
      SignType.neg = SignType.pos ∧ SignType.neg = SignType.pos ∧ EReal.abs x ≤ EReal.abs y

case mp.pos
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.neg ∧ SignType.pos = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.pos = SignType.zero ∧ SignType.pos = SignType.zero ∨
      SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
case mp
x y : EReal
h : ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
⊢ ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
      ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
cases hy : sign y <;> rw [hs, hy] at h ⊢
no goals
case mp.zero
x y : EReal
h : ↑SignType.zero * ↑(EReal.abs x) ≤ ↑SignType.zero * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.zero
⊢ SignType.zero = SignType.neg ∧ SignType.zero = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.zero = SignType.zero ∧ SignType.zero = SignType.zero ∨
      SignType.zero = SignType.pos ∧ SignType.zero = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
simp
case mp.neg.h
x y : EReal
h : ↑SignType.neg * ↑(EReal.abs x) ≤ ↑SignType.neg * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.neg
⊢ SignType.neg = SignType.neg ∧ SignType.neg = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
case mp.neg
x y : EReal
h : ↑SignType.neg * ↑(EReal.abs x) ≤ ↑SignType.neg * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.neg
⊢ SignType.neg = SignType.neg ∧ SignType.neg = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.neg = SignType.zero ∧ SignType.neg = SignType.zero ∨
      SignType.neg = SignType.pos ∧ SignType.neg = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
left
no goals
case mp.neg.h
x y : EReal
h : ↑SignType.neg * ↑(EReal.abs x) ≤ ↑SignType.neg * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.neg
⊢ SignType.neg = SignType.neg ∧ SignType.neg = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
simpa using h
case mp.pos.h
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.zero ∧ SignType.pos = SignType.zero ∨
    SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
case mp.pos
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.neg ∧ SignType.pos = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.pos = SignType.zero ∧ SignType.pos = SignType.zero ∨
      SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
right
case mp.pos.h.h
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
case mp.pos.h
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.zero ∧ SignType.pos = SignType.zero ∨
    SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
right
no goals
case mp.pos.h.h
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
simpa using h
case mpr.inl
x y : EReal
h : ↑sign x < ↑sign y
⊢ x ≤ y

case mpr.inr.inl
x y : EReal
h : ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
⊢ x ≤ y

case mpr.inr.inr.inl
x y : EReal
h : ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero
⊢ x ≤ y

case mpr.inr.inr.inr
x y : EReal
h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
⊢ x ≤ y
case mpr
x y : EReal
⊢ ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y →
    x ≤ y
rintro (h | h | h | h)
no goals
case mpr.inr.inl
x y : EReal
h : ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
⊢ x ≤ y

case mpr.inr.inr.inl
x y : EReal
h : ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero
⊢ x ≤ y

case mpr.inr.inr.inr
x y : EReal
h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
⊢ x ≤ y
all_goals rw [← x.sign_mul_abs, ← y.sign_mul_abs]; simp [h]
no goals
case mpr.inl
x y : EReal
h : ↑sign x < ↑sign y
⊢ x ≤ y
exact (sign.monotone.reflect_lt h).le
case mpr.inr.inr.inr
x y : EReal
h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
⊢ ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
case mpr.inr.inr.inr
x y : EReal
h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
⊢ x ≤ y
rw [← x.sign_mul_abs, ← y.sign_mul_abs]
no goals
case mpr.inr.inr.inr
x y : EReal
h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
⊢ ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
simp [h]