-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
t u : Set α
P : Partition u
f₀ : (↑t : Type u_1) → α
h_notMem : ∀ (x : (↑t : Type u_1)), (↑x : α) ∉ u → f₀ x = (↑x : α)
h_mem : ∀ (x : (↑t : Type u_1)), (↑x : α) ∈ u → P.Rel (s := u) (↑x : α) (f₀ x)
h_eq : ∀ (x y : (↑t : Type u_1)), P.Rel (s := u) (↑x : α) (↑y : α) → f₀ x = f₀ y
set set₁ : ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
set₂ :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a),
    ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
refine_1 :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : α) (ha : a ∈ u), P.Rel (s := u) a (f a)
refine_2 :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a b : α) (hab : P.Rel (s := u) a b), f a = f b
refine_3 :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : (↑t : Type u_1)), f (↑a : α) = f₀ a
refine_2₁ :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a b : α) (hab : P.Rel (s := u) a b), f a = f b
refine_3₁ refine_3₂ :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : (↑t : Type u_1)), f (↑a : α) = f₀ a
refine_3₃ :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : (↑t : Type u_1)) (ha : (↑a : α) ∉ u), f (↑a : α) = f₀ a
refine_3₄ refine_3₅ :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : (↑t : Type u_1)) (ha : (↑a : α) ∈ u), f (↑a : α) = f₀ a
refine_3₆ :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : (↑t : Type u_1)) (ha : (↑a : α) ∈ u),
    (if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) (↑a : α) (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) (↑a : α) (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) (↑a : α)) ⋯) =
      f₀ a
pos :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : (↑t : Type u_1)) (ha : (↑a : α) ∈ u) (h : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) (↑a : α) (↑b : α)),
    f₀ (h.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) (↑a : α) (↑b : α))) = f₀ a
neg neg₁ :
  let f : α → α := fun (a : α) ↦
    if ha : a ∈ u then
      if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
        f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
      else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
    else a;
  ∀
    (hfdef :
      f = fun (a : α) ↦
        if ha : a ∈ u then
          if hb : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α) then
            f₀ (hb.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α)))
          else P.rep (u := u) (t := P.partOf (u := u) a) ⋯
        else a)
    (a : (↑t : Type u_1)) (ha : (↑a : α) ∈ u) (h : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) (↑a : α) (↑b : α)),
    P.rep (u := u) (t := P.partOf (u := u) (↑a : α)) ⋯ = f₀ a
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x

Tactic:
classical
  set f : α → α := fun a ↦ if ha : a ∈ u then
    (if hb : ∃ b : t, P.Rel a b then f₀ hb.choose else P.rep (P.partOf_mem ha)) else a with hfdef
  refine ⟨f, ⟨fun a ha ↦ by simp [hfdef, ha], fun a ha ↦ ?_, fun a b hab ↦ ?_⟩, fun a ↦ ?_⟩
  · simp only [hfdef, ha, ↓reduceDIte]
    split_ifs with h
    · exact h.choose_spec.trans <| h_mem h.choose h.choose_spec.right_mem
    push Not at h
    exact P.rep_rel (P.partOf_mem ha) (P.mem_partOf ha)
  · simp_rw [hfdef, dif_pos hab.left_mem, dif_pos hab.right_mem]
    split_ifs with h₁ h₂ h₂
    · exact h_eq _ _ <| (hab.symm.trans h₁.choose_spec).symm.trans h₂.choose_spec
    · exact h₂ ⟨_, hab.symm.trans h₁.choose_spec⟩ |>.elim
    · exact h₁ ⟨_, hab.trans h₂.choose_spec⟩ |>.elim
    congr 1
    rwa [← rel_iff_partOf_eq_partOf_of_mem _ hab.left_mem hab.right_mem]
  obtain (ha | ha) := em (a.1 ∈ u) |>.symm
  · simp [hfdef, ha, h_notMem _ ha]
  simp only [hfdef, ha, ↓reduceDIte]
  split_ifs with h
  · exact h_eq _ _ h.choose_spec |>.symm
  exact h ⟨a, rel_rfl_iff.mpr ha⟩ |>.elim

Premises used: reduceDIte, Not