awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) ⋯
have neg : P.partOf (u := u) a = P.partOf (u := u) b
Tactic: congr 1
-- 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 : (↑t : Type u_1)
⊢ f (↑a : α) = f₀ a
have refine_3 : ∀ (ha : (↑a : α) ∉ u), f (↑a : α) = f₀ a
Tactic: obtain (ha | ha) := em (a.1 ∈ u) |>.symm
-- 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 : (↑t : Type u_1)
refine_3 : ∀ (ha : (↑a : α) ∉ u), f (↑a : α) = f₀ a
⊢ f (↑a : α) = f₀ a
have refine_3₁ : ∀ (ha : (↑a : α) ∈ u), f (↑a : α) = f₀ a
Tactic: obtain (ha | ha) := em (a.1 ∈ u) |>.symm
-- 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 : (↑t : Type u_1)
ha : (↑a : α) ∈ u
⊢ f (↑a : α) = f₀ a
have refine_3 : (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) =
  f₀ a
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 : (↑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
have pos : ∀ (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
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 : (↑t : Type u_1)
ha : (↑a : α) ∈ u
pos :
  ∀ (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
⊢ (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
have neg : ∀ (h : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) (↑a : α) (↑b : α)),
  P.rep (u := u) (t := P.partOf (u := u) (↑a : α)) sorry = f₀ a
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
set set₁ : ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
have 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) sorry
  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) sorry
      else 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
-- 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
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
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ ∀ (x : (↑t : Type u_1)), f (↑x : α) = f₀ x
have 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) sorry
  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) sorry
      else a)
  (a : α) (ha : a ∈ u), P.Rel (s := u) a (f a)
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
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f
have obtain : ∀ (f : α → α) (hf : P.IsRepFun (u := u) f), ∃ (f : α → α), P.IsRepFun (u := u) f
Tactic: obtain ⟨f, hf, -⟩ := exists_extend_partial' P (t := ∅) (by simp)
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.IsEquipartition ↔ ∀ a ∈ P.parts, #a = #s / #P.parts ∨ #a = #s / #P.parts + 1
have simp_rw : (↑P.parts : Set (Finset α)).EquitableOn Finset.card ↔ ∀ a ∈ P.parts, #a = #s / #P.parts ∨ #a = #s / #P.parts + 1
Tactic: simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
simp_rw :
  (↑P.parts : Set (Finset α)).EquitableOn Finset.card ↔ ∀ a ∈ P.parts, #a = #s / #P.parts ∨ #a = #s / #P.parts + 1
⊢ P.IsEquipartition ↔ ∀ a ∈ P.parts, #a = #s / #P.parts ∨ #a = #s / #P.parts + 1
have simp_rw₁ : (∀ a ∈ P.parts, #a = (∑ i ∈ P.parts, #i) / #P.parts ∨ #a = (∑ i ∈ P.parts, #i) / #P.parts + 1) ↔
  ∀ a ∈ P.parts, #a = #s / #P.parts ∨ #a = #s / #P.parts + 1
Tactic: simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1
have a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
Tactic: have a := hP.card_parts_eq_average ht
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #s / #P.parts ≤ #t
have rw : (∑ i ∈ P.parts, #i) / #P.parts ≤ #t
Tactic: rw [← P.sum_card_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ #s / #P.parts + 1
have rw : #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1
Tactic: rw [← P.sum_card_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ {p ∈ P.parts | ¬#p = #s / #P.parts + 1} = {p ∈ P.parts | #p = #s / #P.parts}
have h : ∀ (p : Finset α), p ∈ {p ∈ P.parts | ¬#p = #s / #P.parts + 1} ↔ p ∈ {p ∈ P.parts | #p = #s / #P.parts}
Tactic: ext p
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
⊢ p ∈ {p ∈ P.parts | ¬#p = #s / #P.parts + 1} ↔ p ∈ {p ∈ P.parts | #p = #s / #P.parts}
have h : p ∈ P.parts → (¬#p = #s / #P.parts + 1 ↔ #p = #s / #P.parts)
Tactic: simp only [mem_filter, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
have z : ∑ i ∈ P.parts, #i = #s
Tactic: have z := P.sum_card_parts
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : ∑ i ∈ P.parts, #i = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
have z₁ : #({x ∈ P.parts | #x = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s
Tactic: rw [← sum_filter_add_sum_filter_not (s := P.parts) (p := fun x ↦ #x = #s / #P.parts + 1),
    hP.filter_ne_average_add_one_eq_average, sum_const_nat (m := #s / #P.parts + 1) (by simp),
    sum_const_nat (m := #s / #P.parts) (by simp), ← hP.filter_ne_average_add_one_eq_average,
    mul_add, add_comm, ← add_assoc, ← add_mul, mul_one, add_comm #_,
    card_filter_add_card_filter_not, add_comm] at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
have rw : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s % #P.parts + #P.parts * (#s / #P.parts)
Tactic: rw [← add_left_inj, Nat.mod_add_div, z]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s
rw : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s % #P.parts + #P.parts * (#s / #P.parts)
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
have a : ℕ
Tactic: rw [← add_left_inj, Nat.mod_add_div, z]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s
rw : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s % #P.parts + #P.parts * (#s / #P.parts)
a : ℕ
rw₁ : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
have rw₂ : #s = #s
Tactic: rw [← add_left_inj, Nat.mod_add_div, z]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
| #P.parts - #s % #P.parts
have arg : #P.parts
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
| #P.parts
have rw : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1})
Tactic: rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
| #P.parts - #s % #P.parts
have arg : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1})
Tactic: arg 1
    rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) = #P.parts - #s % #P.parts
have conv_rhs : #({p ∈ P.parts | #p = #s / #P.parts}) =
  #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
Tactic: conv_rhs =>
    arg 1
    rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) =
    #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
have rw : #({p ∈ P.parts | #p = #s / #P.parts}) = #s % #P.parts + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
Tactic: rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
rw : #({p ∈ P.parts | #p = #s / #P.parts}) = #s % #P.parts + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) =
    #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
have rw₁ : #({p ∈ P.parts | #p = #s / #P.parts}) = #({a ∈ P.parts | ¬#a = #s / #P.parts + 1})
Tactic: rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
rw : #({p ∈ P.parts | #p = #s / #P.parts}) = #s % #P.parts + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
rw₁ : #({p ∈ P.parts | #p = #s / #P.parts}) = #({a ∈ P.parts | ¬#a = #s / #P.parts + 1})
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) =
    #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
have rw₂ : #({p ∈ P.parts | #p = #s / #P.parts}) = #({p ∈ P.parts | #p = #s / #P.parts})
Tactic: rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : ↥({p ∈ P.parts | #p = #s / #P.parts + 1}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts + 1}) :=
  {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
⊢ ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
have simp_rw : ∀ (el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)),
  ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
Tactic: simp_rw [mem_filter, hP.card_large_parts_eq_mod] at el
Cleared hypotheses: el
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
⊢ ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
have simp_rw : ∀ (es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)),
  ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
Tactic: simp_rw [mem_filter, hP.card_small_parts_eq_mod] at es
Cleared hypotheses: es
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts }
have apply : ∀ (a : Finset α),
  a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1 ↔
    Membership.mem (α := Finset α) P.parts ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) a : Finset α) ∧
      Finset.card.{u_1} (α := α) ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) a) = #s / #P.parts
Tactic: apply (Equiv.refl _).subtypeEquiv