Jon Eugster
|
fe719fcfd3
|
bump lean4game, update lakefile
|
2025-08-09 01:19:55 +02:00 |
|
Jon Eugster
|
c35d29dcf4
|
make simp_add available in the entire game #54
|
2024-03-18 16:21:49 +01:00 |
|
Jon Eugster
|
1a66069e89
|
do not import all of mathlib
|
2024-03-14 10:38:03 +01:00 |
|
Kevin Buzzard
|
396a350bda
|
use mathlib Apply ... At
|
2024-01-23 19:24:42 +00:00 |
|
joneugster
|
14ce186239
|
pretty-printer for not equal
|
2023-10-28 22:01:03 +02:00 |
|
joneugster
|
a851a29928
|
custom use tactic
|
2023-10-28 11:48:49 +02:00 |
|
Kevin Buzzard
|
cedc46846d
|
add mystical ancient tactic
|
2023-10-23 13:43:48 +01:00 |
|
joneugster
|
1dbfaae51c
|
the tactic of tactics
|
2023-10-15 03:17:30 +02:00 |
|
Jon Eugster
|
5a9bb1c119
|
apply f to h
|
2023-08-06 23:45:04 +02:00 |
|
Jon Eugster
|
836f8f6078
|
import Mathlib.Tactic everywhere
|
2023-08-04 17:14:49 +02:00 |
|
Jon Eugster
|
2604c89284
|
big refactor
|
2023-05-15 15:12:35 +02:00 |
|