Theorem: notpure_cases (Saturn/DPLL.lean)

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
⊢ ¬x = some !b
Tactic:
match b, eqn  with
| true, Or.inr pf =>
   intro hyp
   simp [pf] at hyp
| false, Or.inr pf =>
   intro hyp
   simp [pf] at hyp
| _ , Or.inl pf =>
   intro hyp
   let w := Eq.trans (Eq.symm pf) hyp
   exact Option.noConfusion w
State after:
no goals

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some true
⊢ ¬x = some !true
Tactic:
intro hyp
State after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some true
hyp : x = some !true
⊢ False

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some true
hyp : x = some !true
⊢ False
Tactic:
simp [pf] at hyp
State after:
no goals

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some false
⊢ ¬x = some !false
Tactic:
intro hyp
State after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some false
hyp : x = some !false
⊢ False

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some false
hyp : x = some !false
⊢ False
Tactic:
simp [pf] at hyp
State after:
no goals

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
⊢ ¬x = some !x✝
Tactic:
intro hyp
State after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
⊢ False

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
⊢ False
Tactic:
let w := Eq.trans (Eq.symm pf) hyp
State after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
w : none = some !x✝ := pf.symm.trans hyp
⊢ False

State before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
w : none = some !x✝ := pf.symm.trans hyp
⊢ False
Tactic:
exact Option.noConfusion w
State after:
no goals