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
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57

import Mathlib

open Nat Real Quaternion CoxeterMatrix Lean

def perm_of_gen (n : ℕ) (i : Fin n) : Equiv.Perm (Fin (n + 1)) :=
  Equiv.swap (Fin.castSucc i) (Fin.succ i)

def toPerm (n : ℕ) : CoxeterMatrix.Group (Aₙ n) →* Equiv.Perm (Fin (n + 1)) :=
  PresentedGroup.toGroup (f := perm_of_gen n) (by
    unfold Aₙ relationsSet relation perm_of_gen
    simp
    intro r x y h
    subst h
    split_ifs
    next h =>
      subst h
      simp
    next h =>
      simp
      obtain h|h := h
      · ext i
        simp
        rcases x with ⟨ _ | x, hx ⟩ <;> rcases y with ⟨ _ | x_1, hx_1 ⟩ <;> norm_num [Fin.ext_iff, pow_succ', Equiv.swap_apply_def] at *
        · subst h
          simp_all only [zero_add, reduceAdd]
          rcases i with ⟨ _ | _ | _ | i, hi ⟩ <;> norm_num [pow_three, Equiv.swap_apply_def]
          simp +arith +decide [Fin.ext_iff]
        · grind


  )

lemma toPerm_bij (n : ℕ) : Function.Bijective <| toPerm n := by
  constructor
  · intro a b h
    -- rw [toPerm, PresentedGroup.toGroup] at h

  · intro a

#eval (Aₙ 2).Group

example : Nat.card (Aₙ 2).Group = 6 := by
  unfold Aₙ CoxeterMatrix.Group relationsSet relation
  simp



lemma A2_weyl_group_card : Nat.card (Aₙ 2).Group = 6 := by
  rw [card_eq_of_bijective (toPerm 2) (toPerm_bij 2), card_eq_fintype_card]
  rfl

set_option maxRecDepth 1000

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