Theorem: HTPI.Example_3_2_4_v2 (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:
have h5 : Q → R := h h3
State after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
h5 : Q → R
⊢ False

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

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