Random useless permutatoin stuff that doesn't even work

Changes

1 changed files (+44/-0)

• Perm.lean (new)
  • @@ -0,0 +1,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