1 2 3 4 5
import Lake open Lake DSL package gam_proofs where require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"