Theorem: HTPI.Example_3_2_4_v3 (HTPILib/Chap3.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:
by_contra h4
State after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ False

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

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