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

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

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

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

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