no goals
α : Type u
β : Type v
inst✝ : Add α
a b✝ c✝ d : WithTop α
x y : α
b : WithTop α
c : α
⊢ none + b = ↑c ↔ ∃ a' b', ↑a' = none ∧ ↑b' = b ∧ a' + b' = c
simp [none_eq_top]
no goals
α : Type u
β : Type v
inst✝ : Add α
a✝ b c✝ d : WithTop α
x y a c : α
⊢ Option.some a + none = ↑c ↔ ∃ a' b', ↑a' = Option.some a ∧ ↑b' = none ∧ a' + b' = c
simp [none_eq_top]
no goals
α : Type u
β : Type v
inst✝ : Add α
a✝ b✝ c✝ d : WithTop α
x y a b c : α
⊢ Option.some a + Option.some b = ↑c ↔ ∃ a' b', ↑a' = Option.some a ∧ ↑b' = Option.some b ∧ a' + b' = c
simp only [some_eq_coe, ← coe_add, coe_eq_coe, exists_and_left, exists_eq_left]