awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∉ u
b : α
⊢ a = f b ↔ a = b
have refine_2 : a = f b → a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∉ u
b : α
refine_2 : a = f b → a = b
⊢ a = f b ↔ a = b
have refine_2₁ : a = b → a = f b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
have inl : ∀ (h1 : ∀ (x : α), f a = f x ↔ a = x), f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
Tactic: obtain h1 | h2 := hf.forall_apply_eq_apply_iff a
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
inl : ∀ (h1 : ∀ (x : α), f a = f x ↔ a = x), f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
have inr : ∀ (h2 : ∀ (x : α), f a = f x ↔ P.Rel (s := u) a x),
  f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
Tactic: obtain h1 | h2 := hf.forall_apply_eq_apply_iff a
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h1 : ∀ (x : α), f a = f x ↔ a = x
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
have inl : (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b → f a = f b
Tactic: refine ⟨by grind, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
⊢ f (f a) = f a
have inl : ∀ (ha : a ∈ u), f (f a) = f a
Tactic: obtain (ha | ha) := em (a ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
inl : ∀ (ha : a ∈ u), f (f a) = f a
⊢ f (f a) = f a
have inr : ∀ (ha : a ∉ u), f (f a) = f a
Tactic: obtain (ha | ha) := em (a ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
⊢ f (f a) = f a
have inl : P.Rel (s := u) a (f a)
Tactic: rw [eq_comm, hf.apply_eq_apply_iff_rel ha]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun (u := u) f
hg : P.IsRepFun (u := u) g
x : α
⊢ f (g x) = f x
have inl : ∀ (hx : x ∈ u), f (g x) = f x
Tactic: obtain (hx | hx) := em (x ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun (u := u) f
hg : P.IsRepFun (u := u) g
x : α
inl : ∀ (hx : x ∈ u), f (g x) = f x
⊢ f (g x) = f x
have inr : ∀ (hx : x ∉ u), f (g x) = f x
Tactic: obtain (hx | hx) := em (x ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
have inr : f x = f x
Tactic: rw [hg.apply_of_notMem hx, hf.apply_of_notMem hx]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ f (g x) = f x
have inr₁ : x = x
Tactic: rw [hg.apply_of_notMem hx, hf.apply_of_notMem hx]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
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 : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
have hfdef : 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) sorry
  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) sorry
  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
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
have refine_1 : ∀ (a : α) (ha : a ∈ u), P.Rel (s := u) a (f a)
Tactic: refine ⟨f, ⟨fun a ha ↦ by simp [hfdef, ha], fun a ha ↦ ?_, fun a b hab ↦ ?_⟩, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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)
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
have refine_2 : ∀ (a b : α) (hab : P.Rel (s := u) a b), f a = f b
Tactic: refine ⟨f, ⟨fun a ha ↦ by simp [hfdef, ha], fun a ha ↦ ?_, fun a b hab ↦ ?_⟩, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
have refine_3 : ∀ (a : (↑t : Type u_1)), f (↑a : α) = f₀ a
Tactic: refine ⟨f, ⟨fun a ha ↦ by simp [hfdef, ha], fun a ha ↦ ?_, fun a b hab ↦ ?_⟩, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ P.Rel (s := u) a (f a)
have 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) sorry)
Tactic: simp only [hfdef, ha, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ 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) ⋯)
have 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 : α))))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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 : α))))
⊢ 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) ⋯)
have 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) sorry)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
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) ⋯)
have h₁ : ∀ (b : (↑t : Type u_1)), ¬P.Rel (s := u) a (↑b : α)
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ f a = f b
have 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) sorry)
  (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) sorry)
Tactic: simp_rw [hfdef, dif_pos hab.left_mem, dif_pos hab.right_mem]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ 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) ⋯)
have 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 : α)))
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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 : α)))
⊢ 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) ⋯)
have 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) sorry
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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) ⋯
⊢ 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) ⋯)
have 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) sorry =
    f₀ (h₂.choose (p := fun (b_1 : (↑t : Type u_1)) ↦ P.Rel (s := u) b (↑b_1 : α)))
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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 : α)))
⊢ 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) ⋯)
have 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) sorry = P.rep (u := u) (t := P.partOf (u := u) b) sorry
Tactic: split_ifs with h₁ h₂ h₂