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

import Mathlib

open Nat Quaternion Real CoxeterMatrix Lean

set_option maxRecDepth 1000

lemma A2_weyl_group_card : Nat.card (Aₙ 2).Group = 6 := by
  -- TODO
  sorry

example : minFac '⓫'.toNat|>λ_11↦(·+97)<$>[0/0,_11,-(⟨1,0,2,4⟩:ℍ[ℤ])^2|>.re.toNat,defaultMaxRecDepth%101,catalan 4,_11,(φ∘φ∘φ∘φ∘φ∘φ<|4‼‼)!,↑((4:Fin 24)-6),⌈deriv (sin ·^69) π⌉₊,_11,Nat.card<|Aₙ 2|>.Group]
    = "anthonywang".toList.map Char.toNat := by
  simp [minFac, minFacAux, defaultMaxRecDepth, catalan_eq_centralBinom_div, A2_weyl_group_card]
  decide