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

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

State before:
case inl
a b c d : Int
p q : Prop
hnq : ¬q
hp : p
⊢ p
Tactic:
exact hp
State after:
no goals

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