Theorem: Option.some_subseteq (Pdl/LocalTableau.lean)

State before:
α : Type u_1
x : α
O : Option α
⊢ some x ⊆ O ↔ some x = O
Tactic:
cases O
State after:
case none
α : Type u_1
x : α
⊢ some x ⊆ none ↔ some x = none

case some
α : Type u_1
x val✝ : α
⊢ some x ⊆ some val✝ ↔ some x = some val✝

State before:
case none
α : Type u_1
x : α
⊢ some x ⊆ none ↔ some x = none

case some
α : Type u_1
x val✝ : α
⊢ some x ⊆ some val✝ ↔ some x = some val✝
Tactic:
all_goals simp
State after:
no goals

State before:
case some
α : Type u_1
x val✝ : α
⊢ some x ⊆ some val✝ ↔ some x = some val✝
Tactic:
simp
State after:
no goals