α : Type ?u.468735
m n : Num
this : Ordering.casesOn (cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ cmp m n = Ordering.eq ↔ m = n
α : Type ?u.468735
m n : Num
⊢ cmp m n = Ordering.eq ↔ m = n
have := cmp_to_nat m n
α : Type ?u.468735
m n : Num
⊢ Ordering.casesOn (cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m) → (cmp m n = Ordering.eq ↔ m = n)
α : Type ?u.468735
m n : Num
this : Ordering.casesOn (cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ cmp m n = Ordering.eq ↔ m = n
revert this
no goals
α : Type ?u.468735
m n : Num
⊢ Ordering.casesOn (cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m) → (cmp m n = Ordering.eq ↔ m = n)
cases cmp m n <;> intro this <;> simp at this ⊢ <;> try { exact this } <;>
simp [show m ≠ n from fun e => by rw [e] at this; exact lt_irrefl _ this]
α : Type ?u.468735
m n : Num
this : ↑n < ↑n
e : m = n
⊢ False
α : Type ?u.468735
m n : Num
this : ↑n < ↑m
e : m = n
⊢ False
rw [e] at this
no goals
α : Type ?u.468735
m n : Num
this : ↑n < ↑n
e : m = n
⊢ False
exact lt_irrefl _ this