Theorem: HTPI.Example_3_2_4 (HTPILib/IntroLean.lean)

State before:
P Q R : Prop
h : P → Q → R
⊢ ¬R → P → ¬Q
Tactic:
assume h2 : ¬R
State after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q

State before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q
Tactic:
assume h3 : P
State after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q

State before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q
Tactic:
have h4 : Q → R := h h3
State after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q → R
⊢ ¬Q

State before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q → R
⊢ ¬Q
Tactic:
contrapos at h4
State after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : ¬R → ¬Q
⊢ ¬Q

State before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : ¬R → ¬Q
⊢ ¬Q
Tactic:
show ¬Q from h4 h2
State after:
no goals