topoSort_perm

formal source

  88    simpa using this
  89
  90/-- `topoSort` covers exactly the elements of `H` with no duplicates. -/
  91lemma topoSort_perm
  92    (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
  93    (wf : WellFounded prec) (H : Finset E) :
  94    (topoSort (E:=E) prec wf H).Pairwise (· ≠ ·) ∧
  95    (topoSort (E:=E) prec wf H).toFinset = H := by
  96  classical
  97  have hAux : ∀ n, ∀ H : Finset E, H.card = n →
  98      (topoSort (E:=E) prec wf H).Pairwise (· ≠ ·) ∧
  99      (topoSort (E:=E) prec wf H).toFinset = H := by
 100    refine Nat.rec ?base ?step
 101    · intro H hcard
 102      have hH : H = (∅ : Finset E) :=
 103        Finset.card_eq_zero.mp (by simpa [hcard] : H.card = 0)
 104      have hTop : topoSort (E:=E) prec wf H = [] := by
 105        simp [topoSort, hH]
 106      simpa [hTop, hH]
 107    · intro n ih H hcard
 108      have hnpos : 0 < H.card := by
 109        simpa [hcard] using Nat.succ_pos n
 110      have hn : H.Nonempty := Finset.card_pos.mp hnpos
 111      obtain ⟨e, heH, hmin⟩ := exists_minimal_in (E:=E) prec wf hn
 112      have hcard' : (H.erase e).card = n := by
 113        have : (H.erase e).card + 1 = H.card := Finset.card_erase_add_one heH
 114        have : (H.erase e).card + 1 = n + 1 := by simpa [hcard] using this
 115        exact Nat.succ.inj this
 116      have htail := ih (H.erase e) hcard'
 117      set tail := topoSort (E:=E) prec wf (H.erase e)
 118      have hTop : topoSort (E:=E) prec wf H = e :: tail := by
 119        simp [topoSort, hn, heH, hmin]
 120      have hxneq : ∀ x ∈ tail, x ≠ e := by
 121        intro x hx