Lean 3 | Lean 4 | requires |
---|---|---|
all_goals | all_goals | [core] |
any_goals | any_goals | [core] |
apply | apply | [core] |
assumption | assumption | [core] |
by_cases | by_cases | [core] |
by_contradiction | by_contra | import Std.Tactic.Basic |
by_contra | by_contra | import Std.Tactic.Basic |
by_contra' | by_contra' | import Mathlib.Tactic.ByContra |
cases | cases' | import Mathlib.Tactic.Cases |
congr | congr | [core] |
contradiction | contradiction | [core] |
contrapose | contrapose | import Mathlib.Tactic.Contrapose |
convert | convert | import Mathlib.Tactic.Convert |
convert_to | convert_to | import Mathlib.Tactic.Convert |
exact | exact | [core] |
exfalso | exfalso | [core] |
field_simp | field_simp | import Mathlib.Tactic.FieldSimp |
finish | — | — |
have | have | import Mathlib.Tactic.Have |
hint | hint | import Mathlib.Tactic.Hint |
induction | induction' | import Mathlib.Tactic.Cases |
intro | intro | [core] |
intros | intro | [core] |
iterate | iterate | [core] |
left | left | [core] |
library_search | exact? | [core] |
linarith | linarith | import Mathlib.Tactic.Linarith |
omega | omega | [core] |
push_neg | push_neg | import Mathlib.Tactic.PushNeg |
rcases | rcases | [core] |
refl | rfl | [core] |
repeat | repeat' | [core] |
right | right | [core] |
ring | ring | import Mathlib.Tactic.Ring |
rintro | rintro | [core] |
rw | rw | [core] |
simp | simp | [core] |
sorry | sorry | [core] |
specialize | specialize | [core] |
split | constructor | [core] |
split_ifs | split | [core] |
squeeze_simp | simp? | [core] |
suggest | apply? | [core] |
swap | swap | import Mathlib.Tactic.PermuteGoals |
symmetry | symm | import Mathlib.Tactic.Relation.Symm |
tauto | tauto | import Mathlib.Tactic.Tauto |
try | try | [core] |
unfold | unfold | [core] |
use | use | import Mathlib.Tactic.Use |
-
Notifications
You must be signed in to change notification settings - Fork 2
Reference sheet for people who know Lean 3 and want to write tactic-based proofs in Lean 4
License
madvorak/lean3-tactic-lean4
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
About
Reference sheet for people who know Lean 3 and want to write tactic-based proofs in Lean 4