Set ind

theorem set_ind {P : S → Prop}    (hemp : P ∅)    (hadd : ∀ x X, x ∉ X → P X → P (insert x X))    (X : S) : P X := by  apply WellFounded.induction set_wf X  intro Y IH  by_cases hempty : size Y = 0  · rw [size_empty] at hempty    subst hempty    apply hemp  · obtain ⟨x, hmem⟩ := set_choose Y hempty    let Y' := Y \ {x}    have hnotin : x ∉ Y' := by      subst Y'      simp [mem_diff, mem_singleton]    have hPY' : P Y' := by      apply IH      subst Y'      rw [ssubset_subset]      constructor      · intro p; rw [mem_diff, mem_singleton]        grind only      · intro H; rw [<-H] at hmem        rw [mem_diff, mem_singleton] at hmem        exact hmem.right rfl    have heq : Y =  {x} ∪ Y' := by      ext z      subst Y'      rw [mem_union, mem_singleton, mem_diff, mem_singleton]      rw [mem_diff, mem_singleton] at hnotin      grind    have : P ({x} ∪ Y') := by      rw [singleton_insert, insert_union_comm, union_empty_left]      apply hadd      · subst Y'; rw [mem_diff, mem_singleton]        rintro ⟨_, H⟩; apply H rfl      · assumption    rw [heq]    exact this