[GOAL]
n m : WithBot ℕ
⊢ n + m = 0 ↔ n = 0 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 0 ↔ none = 0 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 0 ↔ none = 0 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 0 ↔ some val✝ = 0 ∧ none = 0
case some.some val✝¹ val✝ : ℕ ⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
any_goals (exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩)
[GOAL]
case none.none
⊢ none + none = 0 ↔ none = 0 ∧ none = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 0 ↔ none = 0 ∧ some val✝ = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 0 ↔ some val✝ = 0 ∧ none = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 0 ↔ some val✝ = 0 ∧ none = 0
case some.some val✝¹ val✝ : ℕ ⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.2⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
[PROOFSTEP]
exact add_eq_zero_iff' (zero_le _) (zero_le _)
[GOAL]
n m : WithBot ℕ
⊢ n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 1 ↔ none = 0 ∧ none = 1 ∨ none = 1 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 1 ↔ none = 0 ∧ some val✝ = 1 ∨ none = 1 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 1 ↔ some val✝ = 0 ∧ none = 1 ∨ some val✝ = 1 ∧ none = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop
[GOAL]
case none.none
⊢ none + none = 1 ↔ none = 0 ∧ none = 1 ∨ none = 1 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.none
h : none = 0 ∧ none = 1 ∨ none = 1 ∧ none = 0
⊢ none + none = 1
[PROOFSTEP]
aesop
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 1 ↔ none = 0 ∧ some val✝ = 1 ∨ none = 1 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.some
val✝ : ℕ
h : none = 0 ∧ some val✝ = 1 ∨ none = 1 ∧ some val✝ = 0
⊢ none + some val✝ = 1
[PROOFSTEP]
aesop
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 1 ↔ some val✝ = 0 ∧ none = 1 ∨ some val✝ = 1 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ = 0 ∧ none = 1 ∨ some val✝ = 1 ∧ none = 0
⊢ some val✝ + none = 1
[PROOFSTEP]
aesop
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ val✝¹ = 1 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ val✝¹ = 1 ∧ val✝ = 0
[PROOFSTEP]
exact Nat.add_eq_one_iff
[GOAL]
n m : WithBot ℕ
⊢ n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 2 ↔ none = 0 ∧ none = 2 ∨ none = 1 ∧ none = 1 ∨ none = 2 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 2 ↔ none = 0 ∧ some val✝ = 2 ∨ none = 1 ∧ some val✝ = 1 ∨ none = 2 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 2 ↔ some val✝ = 0 ∧ none = 2 ∨ some val✝ = 1 ∧ none = 1 ∨ some val✝ = 2 ∧ none = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop
[GOAL]
case none.none
⊢ none + none = 2 ↔ none = 0 ∧ none = 2 ∨ none = 1 ∧ none = 1 ∨ none = 2 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.none
h : none = 0 ∧ none = 2 ∨ none = 1 ∧ none = 1 ∨ none = 2 ∧ none = 0
⊢ none + none = 2
[PROOFSTEP]
aesop
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 2 ↔ none = 0 ∧ some val✝ = 2 ∨ none = 1 ∧ some val✝ = 1 ∨ none = 2 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.some
val✝ : ℕ
h : none = 0 ∧ some val✝ = 2 ∨ none = 1 ∧ some val✝ = 1 ∨ none = 2 ∧ some val✝ = 0
⊢ none + some val✝ = 2
[PROOFSTEP]
aesop
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 2 ↔ some val✝ = 0 ∧ none = 2 ∨ some val✝ = 1 ∧ none = 1 ∨ some val✝ = 2 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ = 0 ∧ none = 2 ∨ some val✝ = 1 ∧ none = 1 ∨ some val✝ = 2 ∧ none = 0
⊢ some val✝ + none = 2
[PROOFSTEP]
aesop
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    val✝¹ = 0 ∧ val✝ = ↑2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ val✝¹ = ↑2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ val✝¹ = ↑2 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ val✝¹ = ↑2 ∧ val✝ = 0
[PROOFSTEP]
exact Nat.add_eq_two_iff
[GOAL]
n m : WithBot ℕ
⊢ n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 3 ↔ none = 0 ∧ none = 3 ∨ none = 1 ∧ none = 2 ∨ none = 2 ∧ none = 1 ∨ none = 3 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 3 ↔
    none = 0 ∧ some val✝ = 3 ∨ none = 1 ∧ some val✝ = 2 ∨ none = 2 ∧ some val✝ = 1 ∨ none = 3 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 3 ↔
    some val✝ = 0 ∧ none = 3 ∨ some val✝ = 1 ∧ none = 2 ∨ some val✝ = 2 ∧ none = 1 ∨ some val✝ = 3 ∧ none = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop
[GOAL]
case none.none
⊢ none + none = 3 ↔ none = 0 ∧ none = 3 ∨ none = 1 ∧ none = 2 ∨ none = 2 ∧ none = 1 ∨ none = 3 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.none
h : none = 0 ∧ none = 3 ∨ none = 1 ∧ none = 2 ∨ none = 2 ∧ none = 1 ∨ none = 3 ∧ none = 0
⊢ none + none = 3
[PROOFSTEP]
aesop
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 3 ↔
    none = 0 ∧ some val✝ = 3 ∨ none = 1 ∧ some val✝ = 2 ∨ none = 2 ∧ some val✝ = 1 ∨ none = 3 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.some
val✝ : ℕ
h : none = 0 ∧ some val✝ = 3 ∨ none = 1 ∧ some val✝ = 2 ∨ none = 2 ∧ some val✝ = 1 ∨ none = 3 ∧ some val✝ = 0
⊢ none + some val✝ = 3
[PROOFSTEP]
aesop
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 3 ↔
    some val✝ = 0 ∧ none = 3 ∨ some val✝ = 1 ∧ none = 2 ∨ some val✝ = 2 ∧ none = 1 ∨ some val✝ = 3 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ = 0 ∧ none = 3 ∨ some val✝ = 1 ∧ none = 2 ∨ some val✝ = 2 ∧ none = 1 ∨ some val✝ = 3 ∧ none = 0
⊢ some val✝ + none = 3
[PROOFSTEP]
aesop
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ val✝¹ = ↑3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ val✝¹ = ↑3 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ val✝¹ = ↑3 ∧ val✝ = 0
[PROOFSTEP]
exact Nat.add_eq_three_iff
[GOAL]
n : ℕ
⊢ 0 ≤ ↑n
[PROOFSTEP]
rw [← WithBot.coe_zero]
[GOAL]
n : ℕ
⊢ ↑0 ≤ ↑n
[PROOFSTEP]
exact WithBot.coe_le_coe.mpr (Nat.zero_le n)
[GOAL]
n : WithBot ℕ
⊢ n < 0 ↔ n = ⊥
[PROOFSTEP]
refine' Option.casesOn n _ _
[GOAL]
case refine'_1
n : WithBot ℕ
⊢ none < 0 ↔ none = ⊥
case refine'_2 n : WithBot ℕ ⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
[PROOFSTEP]
exact of_eq_true (eq_true_of_decide (Eq.refl true))
[GOAL]
case refine'_2
n : WithBot ℕ
⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
[PROOFSTEP]
intro n
[GOAL]
case refine'_2
n✝ : WithBot ℕ
n : ℕ
⊢ some n < 0 ↔ some n = ⊥
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
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
[PROOFSTEP]
exfalso
[GOAL]
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : some n < 0
⊢ False
[PROOFSTEP]
rw [WithBot.some_eq_coe] at h 
[GOAL]
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : ↑n < 0
⊢ False
[PROOFSTEP]
exact not_le_of_lt h WithBot.coe_nonneg
[GOAL]
case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ some n < 0
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ ⊥ < 0
[PROOFSTEP]
exact of_eq_true (eq_true_of_decide (Eq.refl true))
[GOAL]
x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x
[PROOFSTEP]
refine' ⟨fun h => lt_of_lt_of_le (WithBot.coe_lt_coe.mpr zero_lt_one) h, fun h => _⟩
[GOAL]
x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x
[PROOFSTEP]
induction x using WithBot.recBotCoe
[GOAL]
case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝
[PROOFSTEP]
exact WithBot.coe_le_coe.mpr (Nat.succ_le_iff.mpr (WithBot.coe_lt_coe.mp h))
[GOAL]
x : WithBot ℕ
⊢ ¬x < 1 ↔ ¬x ≤ 0
[PROOFSTEP]
simpa using one_le_iff_zero_lt
[GOAL]
n m : WithBot ℕ
h : n < m
⊢ n + 1 ≤ m
[PROOFSTEP]
cases n
[GOAL]
case none
m : WithBot ℕ
h : none < m
⊢ none + 1 ≤ m
[PROOFSTEP]
exact bot_le
[GOAL]
case some
m : WithBot ℕ
val✝ : ℕ
h : some val✝ < m
⊢ some val✝ + 1 ≤ m
[PROOFSTEP]
cases m
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ < none
⊢ some val✝ + 1 ≤ none
case some.some val✝¹ val✝ : ℕ h : some val✝¹ < some val✝ ⊢ some val✝¹ + 1 ≤ some val✝
[PROOFSTEP]
exacts [(not_lt_bot h).elim, WithBot.some_le_some.2 (WithBot.some_lt_some.1 h)]
