Fix indentation in Homepage.lean

Changes

1 changed files (+1/-1)

• Homepage.lean
  • @@ -14,6 +14,6 @@ instance : Coe Int Nat where
    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 + (·+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] decide