topoSort_perm

proof body

Tactic-mode proof.

  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
 122        have hxErase : x ∈ H.erase e := by
 123          have : x ∈ tail.toFinset := by
 124            simpa using List.mem_toFinset.mpr hx
 125          simpa [tail, htail.2] using this
 126        exact (Finset.mem_erase.mp hxErase).1
 127      have hxneq' : ∀ x ∈ tail, e ≠ x := by
 128        intro x hx
 129        have hxne := hxneq x hx
 130        exact fun h => hxne h.symm
 131      have pairTail : tail.Pairwise (· ≠ ·) := by
 132        simpa [tail] using htail.1
 133      refine And.intro ?pair ?cover
 134      · exact List.Pairwise.cons.2 ⟨hxneq', pairTail⟩
 135      · simp [hTop, tail, htail.2, Finset.insert_erase, heH]
 136  exact hAux H.card H rfl
 137
 138/-- Respect of precedence: earlier elements in `topoSort` have no incoming edges from later ones. -/