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

State before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ U
Tactic:
apply l
State after:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ T

State before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ T
Tactic:
apply j
State after:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ Q

State before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ Q
Tactic:
apply h
State after:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ P

State before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ P
Tactic:
exact p
State after:
no goals