Theorem: Smt.Reconstruct.Prop.orImplies₃ (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {p q : Prop}, p ∨ q → ¬p → q
Tactic:
intros P Q h np
State after:
P Q : Prop
h : P ∨ Q
np : ¬P
⊢ Q

State before:
P Q : Prop
h : P ∨ Q
np : ¬P
⊢ Q
Tactic:
cases h with
| inl p => exact False.elim (np p)
| inr q => exact q
State after:
no goals

State before:
case inl
P Q : Prop
np : ¬P
p : P
⊢ Q
Tactic:
exact False.elim (np p)
State after:
no goals

State before:
case inr
P Q : Prop
np : ¬P
q : Q
⊢ Q
Tactic:
exact q
State after:
no goals