Theorem: MyNat.imp_trans (TheoremProvingLean/inductive_types.lean)

State before:
P Q F : Prop
⊢ (P → Q) → (Q → F) → P → F
Tactic:
intro f g _
State after:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ F

State before:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ F
Tactic:
apply g
State after:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ Q

State before:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ Q
Tactic:
apply f
State after:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ P

State before:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ P
Tactic:
assumption
State after:
no goals