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
n m : WithBot ℕ
⊢ n + m = 0 ↔ n = 0 ∧ m = 0
rcases n, m with ⟨_ | _, _ | _⟩
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
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
any_goals (exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩)
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 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
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.2⟩
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
repeat' erw [WithBot.coe_eq_coe]
no goals
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
exact add_eq_zero_iff' (zero_le _) (zero_le _)
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
(exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩)
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
erw [WithBot.coe_eq_coe]