1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17

import Mathlib

open Equiv Finset Fintype Nat Quaternion Real

instance : Coe Nat Char where
  coe x := Char.ofNat x

instance : Coe Char Nat where
  coe x := x.toNat

instance : Coe Int Nat where
  coe x := x.toNat

example : let _11:=minFac '⓫'
  (·+97)<$>[0/0,_11,-(⟨1,0,2,4⟩:ℍ[ℤ])^2|>.re,2|>λo↦#{o∈Ioo o<|o<<<o|||o|o∣o},catalan 4,_11,(φ 5)!,↑((4:Fin 24)-6),floor<|deriv (sin ·^69) π,_11,card<|Perm<|Fin 3] = "anthonywang".toList := by
  simp [minFac, minFacAux, catalan_eq_centralBinom_div]
  decide