Improve homepage puzzle a bit (but one of the proofs is hard 😭)

Changes

1 changed files (+8/-14)

• Homepage.lean
  • @@ -1,20 +1,14 @@
    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 + open Nat Quaternion Real CoxeterMatrix Lean set_option maxRecDepth 1000 - 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,(φ∘φ∘φ∘φ∘φ∘φ<|4‼‼)!,↑((4:Fin 24)-6),⌈deriv (sin ·^69) π⌉₊,_11,card<|Perm<|Fin 3] - = "anthonywang".toList := by - simp [minFac, minFacAux, catalan_eq_centralBinom_div] + 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