awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun (u := u) f
hg : P.IsRepFun (u := u) g
x : α
hx : x ∈ u
⊢ f (g x) = f x

Tactic:
exact hf.apply_eq_apply (hg.rel_apply hx).symm

Premises used: Partition.IsRepFun.apply_eq_apply, Partition.IsRepFun.rel_apply, Partition.Rel.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun (u := u) f
hg : P.IsRepFun (u := u) g
x : α
hx : x ∉ u
inr : f x = f x
inr₁ inr₂ : x = x
⊢ f (g x) = f x

Tactic:
rw [hg.apply_of_notMem hx, hf.apply_of_notMem hx]

Premises used: Partition.IsRepFun.apply_of_notMem
-- 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
⊢ 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;
  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

Tactic:
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

Premises used: Membership.mem, Exists, dite, Partition.partOf_mem, Exists.choose, Subtype.val, Partition.rep, Partition.Rel
-- 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
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
⊢ f a = a

Tactic:
simp [hfdef, ha]
-- 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
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
refine_1 : ∀ (a : α) (ha : a ∈ u), P.Rel (s := u) a (f a)
refine_2 : ∀ (a b : α) (hab : P.Rel (s := u) a b), f a = f b
refine_3 : ∀ (a : (↑t : Type u_1)), f (↑a : α) = f₀ a
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x

Tactic:
refine ⟨f, ⟨fun a ha ↦ by simp [hfdef, ha], fun a ha ↦ ?_, fun a b hab ↦ ?_⟩, fun a ↦ ?_⟩
-- 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
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
refine_1 :
  P.Rel (s := u) a
    (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) ⋯)
⊢ P.Rel (s := u) a (f a)

Tactic:
simp only [hfdef, ha, ↓reduceDIte]

Premises used: reduceDIte
-- 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
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
pos :
  ∀ (h : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)),
    P.Rel (s := u) a (f₀ (h.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))))
neg :
  ∀ (h : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)),
    P.Rel (s := u) a (P.rep (u := u) (t := P.partOf (u := u) a) ⋯)
⊢ P.Rel (s := u) a
    (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) ⋯)

Tactic:
split_ifs with h
-- 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
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
h : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
⊢ P.Rel (s := u) a (f₀ (h.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))))

Tactic:
h.choose_spec.trans <| h_mem h.choose h.choose_spec.right_mem

Premises used: Exists.choose_spec, Partition.Rel.right_mem, Partition.Rel.trans, Exists.choose
-- 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
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
h : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
⊢ P.Rel (s := u) a (f₀ (h.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))))

Tactic:
exact h.choose_spec.trans <| h_mem h.choose h.choose_spec.right_mem

Premises used: Exists.choose_spec, Partition.Rel.right_mem, Partition.Rel.trans, Exists.choose
-- 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
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
h : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
⊢ ∀ (b : (↑t : Type u_1)), ¬P.Rel (s := u) a (↑b : α)

Tactic:
push Not at h

Premises used: Not
-- 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
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
h : ∀ (b : (↑t : Type u_1)), ¬P.Rel (s := u) a (↑b : α)
⊢ P.Rel (s := u) a (P.rep (u := u) (t := P.partOf (u := u) a) ⋯)

Tactic:
P.rep_rel (P.partOf_mem ha) (P.mem_partOf ha)

Premises used: Partition.rep_rel, Partition.partOf_mem, Partition.mem_partOf
-- 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
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
h : ∀ (b : (↑t : Type u_1)), ¬P.Rel (s := u) a (↑b : α)
⊢ P.Rel (s := u) a (P.rep (u := u) (t := P.partOf (u := u) a) ⋯)

Tactic:
exact P.rep_rel (P.partOf_mem ha) (P.mem_partOf ha)

Premises used: Partition.rep_rel, Partition.partOf_mem, Partition.mem_partOf
-- 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
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
refine_2 :
  Eq.{u_1 + 1} (α := α)
    (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) ⋯)
    (if hb : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α) then
      f₀ (hb.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))
    else P.rep (u := u) (t := P.partOf (u := u) b) ⋯)
⊢ f a = f b

Tactic:
simp_rw [hfdef, dif_pos hab.left_mem, dif_pos hab.right_mem]

Premises used: Partition.Rel.right_mem, dif_pos, Partition.Rel.left_mem
-- 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
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
pos :
  ∀ (h₁ : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α))
    (h₂ : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)),
    f₀ (h₁.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))) =
      f₀ (h₂.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))
neg :
  ∀ (h₁ : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α))
    (h₂ : ¬∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)),
    f₀ (h₁.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))) =
      P.rep (u := u) (t := P.partOf (u := u) b) ⋯
pos₁ :
  ∀ (h₁ : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α))
    (h₂ : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)),
    P.rep (u := u) (t := P.partOf (u := u) a) ⋯ =
      f₀ (h₂.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))
neg₁ :
  ∀ (h₁ : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α))
    (h₂ : ¬∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)),
    P.rep (u := u) (t := P.partOf (u := u) a) ⋯ = P.rep (u := u) (t := P.partOf (u := u) b) ⋯
⊢ Eq.{u_1 + 1} (α := α)
    (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) ⋯)
    (if hb : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α) then
      f₀ (hb.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))
    else P.rep (u := u) (t := P.partOf (u := u) b) ⋯)

Tactic:
split_ifs with h₁ h₂ h₂
-- 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
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
h₁ : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
h₂ : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)
⊢ f₀ (h₁.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))) =
    f₀ (h₂.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))

Tactic:
h_eq _ _ <| (hab.symm.trans h₁.choose_spec).symm.trans h₂.choose_spec

Premises used: Exists.choose_spec, Partition.Rel.trans, Partition.Rel.symm
-- 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
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
h₁ : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
h₂ : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)
⊢ f₀ (h₁.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))) =
    f₀ (h₂.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))

Tactic:
exact h_eq _ _ <| (hab.symm.trans h₁.choose_spec).symm.trans h₂.choose_spec

Premises used: Exists.choose_spec, Partition.Rel.trans, Partition.Rel.symm
-- 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
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
h₁ : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
h₂ : ¬∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)
⊢ f₀ (h₁.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))) =
    P.rep (u := u) (t := P.partOf (u := u) b) ⋯

Tactic:
h₂ ⟨_, hab.symm.trans h₁.choose_spec⟩ |>.elim

Premises used: Exists.choose_spec, False.elim, Partition.Rel.trans, Partition.Rel.symm, Exists.intro
-- 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
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
h₁ : ∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
h₂ : ¬∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)
⊢ f₀ (h₁.choose (p := fun (b : (↑t : Type u_1)) ↦ P.Rel (s := u) a (↑b : α))) =
    P.rep (u := u) (t := P.partOf (u := u) b) ⋯

Tactic:
exact h₂ ⟨_, hab.symm.trans h₁.choose_spec⟩ |>.elim

Premises used: Exists.choose_spec, False.elim, Partition.Rel.trans, Partition.Rel.symm, Exists.intro
-- 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
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
h₁ : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
h₂ : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)
⊢ P.rep (u := u) (t := P.partOf (u := u) a) ⋯ =
    f₀ (h₂.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))

Tactic:
h₁ ⟨_, hab.trans h₂.choose_spec⟩ |>.elim

Premises used: Exists.choose_spec, False.elim, Partition.Rel.trans, Exists.intro
-- 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
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
h₁ : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) a (↑b : α)
h₂ : ∃ (b_1 : (↑t : Type u_1)), P.Rel (s := u) b (↑b_1 : α)
⊢ P.rep (u := u) (t := P.partOf (u := u) a) ⋯ =
    f₀ (h₂.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))

Tactic:
exact h₁ ⟨_, hab.trans h₂.choose_spec⟩ |>.elim

Premises used: Exists.choose_spec, False.elim, Partition.Rel.trans, Exists.intro