Theorem: LoVe.cases_Classical_em_example (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
α : Type
a : α
P Q : α → Prop
⊢ Q a
Tactic:
have hor : P a ∨ ¬ P a :=
  Classical.em (P a)
State after:
α : Type
a : α
P Q : α → Prop
hor : P a ∨ ¬P a
⊢ Q a

State before:
α : Type
a : α
P Q : α → Prop
hor : P a ∨ ¬P a
⊢ Q a
Tactic:
cases hor with
| inl hl => sorry
| inr hr => sorry
State after:
no goals

State before:
case inl
α : Type
a : α
P Q : α → Prop
hl : P a
⊢ Q a
Tactic:
sorry
State after:
no goals

State before:
case inr
α : Type
a : α
P Q : α → Prop
hr : ¬P a
⊢ Q a
Tactic:
sorry
State after:
no goals