Is it possible to see how `metis`

manages to finish a proof?

My current proof ends with:

```
apply (auto simp add: fun_eq_iff morph_comp_def split: if_splits)
apply metis
by metis
```

And I would like to drop the two `metis`

calls.

There are `metis_trace`

and `metis_verbose`

, but I don't know how to read the output,

e.g. `using [[metis_trace]] by metis`

.

Robert Soeldner has marked this topic as resolved.

Last updated: Feb 27 2024 at 08:17 UTC