ultimate tactic

Stream: general

[Patrick Massot]

I found the ultimate Lean tactic: https://stacks.math.columbia.edu/tag/05SG

[Patrick Massot]

I think this is my new favorite Stacks tag

[Sean Leather]

Lemma 4.2.18. Let $F : \mathcal{A} \to \mathcal{B}$ be a fully faithful functor. Suppose for every $X \in Ob(\mathcal{B})$ given an object $j(X)$ of $\mathcal{A}$ and an isomorphism $i_X : X \to F(j(X))$. Then there is a unique functor $j : \mathcal{B} \to \mathcal{A}$ such that $j$ extends the rule on objects, and the isomorphisms $i_X$ define an isomorphism of functors $\text{id}_\mathcal{B} \to F \circ j$. Moreover, $j$ and $F$ are quasi-inverse equivalences of categories.

Proof. This lemma proves itself. $\square$

[Simon Hudon]

I think this recursive proof is not well founded :stuck_out_tongue: