Coq to Lean Tactic Cheatsheet

This is a guide for coq users getting into writing lean proofs.

Please PR your own or request additions via issue tracker or lean gitter.

n/a doesn’t mean it doesn’t exist, only that I don’t know about it.

The main table is for the Lean release v3.3.0.

Coq Tactic	Lean Tactic	Notes
`;`	`;`
`.`	`,`
`assumption`	`assumption`
`admit`	`admit`
`apply`	`apply`	lean `apply` is coq `eapply`
`apply H in A`	`have A2 := H A`	Will create a new hypothesis A2, and A will persist, see coq-tactic-substitutes.lean for a closer approximation
`assert`	`have`
`auto`	n/a
`autorewrite`	n/a	`simp using <attribute>` approximates
`change`	`change`
`change with`	n/a
`clear`	`clear`	no `clear -`
`constructor`	`constructor`
`destruct`	`cases`
`destruct x eqn:?`	`destruct x`
`eapply`	`apply`
`exact`	`exact`
`exfalso`	`exfalso`
`exists`	`existsi`	`use` is the same, but takes the expected type into account. `use` requires mathlib
`eexists`	`existsi _`
`f_equal`	`congr' 1`	requires mathlib
`fail`	`fail_if_success {skip}`
`first [A \\| B \\|.. \\| X]`	`first [A B .. X]`
`generalize t`	`generalize : t = y`	`y` is name of the new variable, the name must be provided
`generalize dependent`	`revert`
`idtac`	`skip`	`skip` does not print, succeeds trivially
`induction`	`induction`
`intro`	`intro`
`intros`	`intros`
`intuition`	n/a
`inversion`	`cases`	Cases should be applied to dependent arguments first
`left`	`left`
`omega`	`omega`	requires mathlib. Might not have the same features as Coq’s `omega`
`pose`	`let`
`pose proof`	`have`
`progress`	n/a	lean tactics by convention should fail if they don’t progress
`remember x as y eqn:h`	`generalize h : x = y`	names must be provided
`revert`	n/a	always dependent
`revert dependent`	`revert`
`rewrite`	`rewrite`, `rw`
`rewrite <-`	`rewrite <-`, `rw`
`right`	`right`
`simpl`	`dsimp`	to some approximation at least. `simp only` might be closer
`simpl in`	`dsimp at`
`simpl in *`	`dsimp at *`
`solve`	`solve1`
`specialize (H e)`	`specialize (H e)`
`split`	`split`
`subst x`	`subst x`
`subst`	n/a
`symmetry`	`symmetry`
`transitivity`	`transitivity`
`trivial`	`trivial`
`try T`	`try {T}`	curly braces required
`typeclasses eauto`	`apply_instance`
`unfold`	`unfold`
`unfold in`	`unfold at`
`unshelve eapply`	`fapply`

Similar options from Coq exist in Lean as well. Whereas Coq options are set and unset with the Vernacular Set option and Unset option, Lean options toggled with set_option <option> true and set_option <option> false. Here is a list of Coq options and their Lean versions:

Coq option	Lean option	Notes
`Printing Implicit`	`pp.implicit`	default `false`
`Printing Universes`	`pp.universes`	default `false`
`Printing Notations`	`pp.notation`	default `true`

And other Vernacular:

Coq Vernacular	Lean directive	Notes
`Opaque ident`	`attribute [irreducible] ident`
`Transparent ident`	`attribute [reducible] ident`
`Check term`	`#check term`
`Print term`	`#print term`	Can also be used to print structures, inductive types, notation
`Proof using P`	`include P`	`include P` makes `P` available to all proofs, as well as typeclass resolution if it is an instance. `omit P` un-includes `P`

Variables and sections

Coq construct	Lean construct	Notes
`Variable`	`parameter`	only within a section. Lean `variable` does not automatically apply arguments within the section
`Universes`	`universes`	use `universe variables` if you want to declare the universes, but not fix them for the file