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

import Mathlib

variable {n} (I : (i : Fin n) → (j : Fin n) → (j < i) → Bool)

def f (i j : Fin n) :=
  if h : i = j then
    false
  else if h : i < j then
    I j i h
  else
    I i j (by grind)

-- def f (i j : Fin n) := match h : compare i j with
--   | .lt => I j i <| compare_lt_iff_lt.mp h
--   | .eq => false
--   | .gt => !(I i j <| compare_gt_iff_gt.mp h)

def w (i : Fin n) := Finset.card {j | f I i j}

example (hI : ∀ i j k, (h₁ : j < i) → (h₂ : k < j) → I i j h₁ → I j k h₂ → I i k (Fin.lt_trans h₂ h₁))
    (hnI : ∀ i j k, (h₁ : j < i) → (h₂ : k < j) → !(I i j h₁) → !(I j k h₂) → !(I i k <| Fin.lt_trans h₂ h₁))
    (hii' : i' < i)
    : w I i ≠ w I i' := by
  unfold w
  by_cases h₁ : f I i i'
  · have blah j : f I i j ≤ f I i' j := by
      have cases : j < i' ∨ j = i' ∨ (i' < j ∧ j < i) ∨ j = i ∨ i < j := by
        grind
      obtain h₂|h₂|h₂|h₂|h₂ := cases
      · unfold f
        -- grind
      · unfold f at h₁ ⊢
        simp [h₂, show i ≠ i' by grind, show ¬ i < i' by grind] at h₁ ⊢
      · sorry
      · unfold f at h₁ ⊢
        simp [h₂, hii', show i ≠ i' by grind] at h₁ ⊢
        grind

      · sorry
    sorry
  · sorry


def blah (x : α) := x