case refine'_1
n : WithBot ℕ
⊢ none < 0 ↔ none = ⊥

case refine'_2
n : WithBot ℕ
⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
n : WithBot ℕ
⊢ n < 0 ↔ n = ⊥
refine' Option.casesOn n _ _
case refine'_2
n : WithBot ℕ
⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
case refine'_1
n : WithBot ℕ
⊢ none < 0 ↔ none = ⊥

case refine'_2
n : WithBot ℕ
⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
exact of_eq_true (eq_true_of_decide (Eq.refl true))
case refine'_2
n✝ : WithBot ℕ
n : ℕ
⊢ some n < 0 ↔ some n = ⊥
case refine'_2
n : WithBot ℕ
⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
intro n
case refine'_2.refine'_1
n✝ : WithBot ℕ
n : ℕ
h : some n < 0
⊢ some n = ⊥

case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ some n < 0
case refine'_2
n✝ : WithBot ℕ
n : ℕ
⊢ some n < 0 ↔ some n = ⊥
refine' ⟨fun h => _, fun h => _⟩
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : some n < 0
⊢ False

case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ some n < 0
case refine'_2.refine'_1
n✝ : WithBot ℕ
n : ℕ
h : some n < 0
⊢ some n = ⊥

case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ some n < 0
exfalso
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : ↑n < 0
⊢ False
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : some n < 0
⊢ False
rw [WithBot.some_eq_coe] at h
no goals
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : ↑n < 0
⊢ False
exact not_le_of_lt h WithBot.coe_nonneg
case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ ⊥ < 0
case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ some n < 0
rw [h]
no goals
case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ ⊥ < 0
exact of_eq_true (eq_true_of_decide (Eq.refl true))