awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ ∀ (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
have simp : ∀ a ∈ P.parts, ¬#a = #s / #P.parts + 1 ↔ #a = #s / #P.parts
Tactic: simp only [Equiv.refl_apply, and_congr_right_iff]
-- 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 α
ha : x ∈ P.parts
⊢ ¬#x = #s / #P.parts + 1 ↔ #x = #s / #P.parts
have rw : ¬#x = #s / #P.parts + 1 ↔ #x ≠ #s / #P.parts + 1
Tactic: rw [hP.card_part_eq_average_iff ha, ne_eq]
-- 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 α
ha : x ∈ P.parts
rw : ¬#x = #s / #P.parts + 1 ↔ #x ≠ #s / #P.parts + 1
⊢ ¬#x = #s / #P.parts + 1 ↔ #x = #s / #P.parts
have rw₁ : ¬#x = #s / #P.parts + 1 ↔ ¬#x = #s / #P.parts + 1
Tactic: rw [hP.card_part_eq_average_iff ha, ne_eq]
-- 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)
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
⊢ ∃ (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 replace : ∀ (el : { x : ↥P.parts // #(↑x : Finset α) = #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: replace el : { x : P.parts // #x.1 = #s / #P.parts + 1 } ≃
      Fin (#s % #P.parts) := (Equiv.Set.sep ..).symm.trans 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 : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #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 replace : ∀ (es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ 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: replace es : { x : P.parts // ¬#x.1 = #s / #P.parts + 1 } ≃
      Fin (#P.parts - #s % #P.parts) := (Equiv.Set.sep ..).symm.trans (sneg.trans 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
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  Equiv.trans (Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1))
    ((el.sumCongr es).trans finSumFinEquiv)
⊢ ∃ (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 h : ∀ (t : ↥P.parts),
  #(↑t : Finset α) = #s / #P.parts + 1 ↔
    (↑((f.trans (finCongr sorry) : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
Tactic: use f.trans (finCongr (Nat.add_sub_of_le P.card_mod_card_parts_le))
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  Equiv.trans (Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1))
    ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property : p ∈ P.parts
⊢ #(↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property) : Finset α) = #s / #P.parts + 1 ↔
    (↑((f.trans (finCongr ⋯) : (a : ↥P.parts) → Fin #P.parts)
            (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)) :
        ℕ) <
      #s % #P.parts
have h : #p = #s / #P.parts + 1 ↔
  (↑((finSumFinEquiv :
            (a : Fin (#s % #P.parts) ⊕ Fin (#P.parts - #s % #P.parts)) →
              Fin (#s % #P.parts + (#P.parts - #s % #P.parts)))
          (Sum.map (α := { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) (β :=
            { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 })
            (⇑el : (a : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#s % #P.parts))
            (⇑es : (a : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#P.parts - #s % #P.parts))
            ((Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1) :
                (a : ↥P.parts) →
                  { a : ↥P.parts // #(↑a : Finset α) = #s / #P.parts + 1 } ⊕
                    { a : ↥P.parts // ¬#(↑a : Finset α) = #s / #P.parts + 1 })
              (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)))) :
      ℕ) <
    #s % #P.parts
Tactic: simp_rw [f, Equiv.trans_apply, Equiv.sumCongr_apply, finCongr_apply, Fin.val_cast]
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  Equiv.trans (Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1))
    ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property : p ∈ P.parts
⊢ #p = #s / #P.parts + 1 ↔
    (↑((finSumFinEquiv :
              (a : Fin (#s % #P.parts) ⊕ Fin (#P.parts - #s % #P.parts)) →
                Fin (#s % #P.parts + (#P.parts - #s % #P.parts)))
            (Sum.map (α := { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) (β :=
              { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 })
              (⇑el : (a : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#s % #P.parts))
              (⇑es : (a : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#P.parts - #s % #P.parts))
              ((Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1) :
                  (a : ↥P.parts) →
                    { a : ↥P.parts // #(↑a : Finset α) = #s / #P.parts + 1 } ⊕
                      { a : ↥P.parts // ¬#(↑a : Finset α) = #s / #P.parts + 1 })
                (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)))) :
        ℕ) <
      #s % #P.parts
have pos : ∀ (hc : #p = #s / #P.parts + 1),
  #p = #s / #P.parts + 1 ↔
    (↑((finSumFinEquiv :
              (a : Fin (#s % #P.parts) ⊕ Fin (#P.parts - #s % #P.parts)) →
                Fin (#s % #P.parts + (#P.parts - #s % #P.parts)))
            (Sum.map (α := { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) (β :=
              { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 })
              (⇑el : (a : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#s % #P.parts))
              (⇑es : (a : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#P.parts - #s % #P.parts))
              ((Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1) :
                  (a : ↥P.parts) →
                    { a : ↥P.parts // #(↑a : Finset α) = #s / #P.parts + 1 } ⊕
                      { a : ↥P.parts // ¬#(↑a : Finset α) = #s / #P.parts + 1 })
                (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)))) :
        ℕ) <
      #s % #P.parts
Tactic: by_cases hc : #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
⊢ ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
have obtain : ∀ (f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α))
  (hf :
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        Eq.{u_1 + 1} (α := ↥P.parts)
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))),
  ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
Tactic: obtain ⟨f, hf⟩ := P.exists_enumeration
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
⊢ ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
have obtain : ∀ (g : ↥P.parts ≃ Fin #P.parts)
  (hg :
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts),
  ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
Tactic: obtain ⟨g, hg⟩ := hP.exists_partsEquiv
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
⊢ ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
have gl : ∀ (a : ↥s),
  (↑((g : (a : ↥P.parts) → Fin #P.parts)
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
      ℕ) <
    #P.parts
Tactic: have gl := fun a ↦ (g (f a).1).2
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
gl :
  ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts
a : ↥s
⊢ z a < #s
have inl : ∀
  (c :
    Finset.card.{u_1} (α := α)
        (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
          Finset α) =
      #s / #P.parts),
  z a < #s
Tactic: rcases hP.card_parts_eq_average (f a).1.2 with (c | c)
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
gl :
  ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts
a : ↥s
inl :
  ∀
    (c :
      Finset.card.{u_1} (α := α)
          (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
            Finset α) =
        #s / #P.parts),
    z a < #s
⊢ z a < #s
have inr : ∀
  (c :
    Finset.card.{u_1} (α := α)
        (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
          Finset α) =
      #s / #P.parts + 1),
  z a < #s
Tactic: rcases hP.card_parts_eq_average (f a).1.2 with (c | c)
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
gl :
  ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts
a : ↥s
c :
  Finset.card.{u_1} (α := α)
      (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
        Finset α) =
    #s / #P.parts
⊢ #P.parts *
      ((↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
        1) ≤
    #P.parts * (#s / #P.parts)
have bc : (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
          Fin
            (Finset.card.{u_1} (α := α)
              (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                    ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                Finset α))) :
      ℕ) +
    1 ≤
  #s / #P.parts
Tactic: gcongr