Theorem: Smt.Reconstruct.Int.or_implies_right (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d : Int
p q : Prop
hpq : p ∨ q
hnp : ¬p
⊢ q
Tactic:
cases hpq with
| inl hp => exact False.elim (hnp hp)
| inr hq => exact hq
State after:
no goals

State before:
case inl
a b c d : Int
p q : Prop
hnp : ¬p
hp : p
⊢ q
Tactic:
exact False.elim (hnp hp)
State after:
no goals

State before:
case inr
a b c d : Int
p q : Prop
hnp : ¬p
hq : q
⊢ q
Tactic:
exact hq
State after:
no goals