awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α)
neg : P.partOf (u := u) a = P.partOf (u := u) b
⊢ P.rep (u := u) (t := P.partOf (u := u) a) ⋯ = P.rep (u := u) (t := P.partOf (u := u) b) ⋯

Tactic:
congr 1
-- 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 : α)
neg neg₁ neg₂ neg₃ : P.Rel (s := u) a b
⊢ P.partOf (u := u) a = P.partOf (u := u) b

Tactic:
rwa [← rel_iff_partOf_eq_partOf_of_mem _ hab.left_mem hab.right_mem]

Premises used: Partition.Rel.right_mem, Partition.Rel.left_mem, Partition.rel_iff_partOf_eq_partOf_of_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 : (↑t : Type u_1)
refine_3 : ∀ (ha : (↑a : α) ∉ u), f (↑a : α) = f₀ a
refine_3₁ : ∀ (ha : (↑a : α) ∈ u), f (↑a : α) = f₀ a
⊢ f (↑a : α) = f₀ a

Tactic:
obtain (ha | ha) := em (a.1 ∈ u) |>.symm

Premises used: Membership.mem, em, Or.symm, Subtype.val
-- 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 : (↑t : Type u_1)
ha : (↑a : α) ∉ u
⊢ f (↑a : α) = f₀ a

Tactic:
simp [hfdef, ha, h_notMem _ 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
a : (↑t : Type u_1)
ha : (↑a : α) ∈ u
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 : α)) ⋯) =
    f₀ a
⊢ f (↑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 : (↑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
neg :
  ∀ (h : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) (↑a : α) (↑b : α)),
    P.rep (u := u) (t := P.partOf (u := u) (↑a : α)) ⋯ = 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

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

Tactic:
h_eq _ _ h.choose_spec |>.symm

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

Tactic:
exact h_eq _ _ h.choose_spec |>.symm

Premises used: Exists.choose_spec, Eq.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 : (↑t : Type u_1)
ha : (↑a : α) ∈ u
h : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) (↑a : α) (↑b : α)
⊢ P.rep (u := u) (t := P.partOf (u := u) (↑a : α)) ⋯ = f₀ a

Tactic:
h ⟨a, rel_rfl_iff.mpr ha⟩ |>.elim

Premises used: Iff.mpr, Partition.rel_rfl_iff, False.elim, 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 : (↑t : Type u_1)
ha : (↑a : α) ∈ u
h : ¬∃ (b : (↑t : Type u_1)), P.Rel (s := u) (↑a : α) (↑b : α)
⊢ P.rep (u := u) (t := P.partOf (u := u) (↑a : α)) ⋯ = f₀ a

Tactic:
exact h ⟨a, rel_rfl_iff.mpr ha⟩ |>.elim

Premises used: Iff.mpr, Partition.rel_rfl_iff, False.elim, Exists.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
t u : Set α
P : Partition u
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel (s := u) x y → x = y
⊢ ∀ (x : (↑t : Type u_1)), (↑x : α) ∉ u → (fun (x : (↑t : Type u_1)) ↦ (↑x : α)) x = (↑x : α)

Tactic:
simp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
t u : Set α
P : Partition u
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel (s := u) x y → x = y
⊢ ∀ (x : (↑t : Type u_1)), (↑x : α) ∈ u → P.Rel (s := u) (↑x : α) ((fun (x : (↑t : Type u_1)) ↦ (↑x : α)) x)

Tactic:
simp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
t u : Set α
P : Partition u
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel (s := u) x y → x = y
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f ∧ EqOn f id t

Tactic:
simpa using exists_extend_partial P (fun x : t ↦ x) (by simp) (by simp) (fun x y ↦ h x.2 y.2)

Premises used: Partition.IsRepFun.exists_extend_partial, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
⊢ ∀ ⦃x y : α⦄, Membership.mem (γ := Set α) ∅ x → Membership.mem (γ := Set α) ∅ y → P.Rel (s := u) x y → x = y

Tactic:
simp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
obtain : ∀ (f : α → α) (hf : P.IsRepFun (u := u) f), ∃ (f : α → α), P.IsRepFun (u := u) f
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f

Tactic:
obtain ⟨f, hf, -⟩ := exists_extend_partial' P (t := ∅) (by simp)

Premises used: Partition.IsRepFun.exists_extend_partial'
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f

Tactic:
⟨f, hf⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
⊢ ∃ (f : α → α), P.IsRepFun (u := u) f

Tactic:
exact ⟨f, hf⟩
-- Module: Mathlib.Order.Partition.Equipartition
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
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
⊢ P.IsEquipartition ↔ ∀ a ∈ P.parts, #a = #s / #P.parts ∨ #a = #s / #P.parts + 1

Tactic:
simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]

Premises used: Finset.equitableOn_iff, Finpartition.sum_card_parts, Finpartition.IsEquipartition
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ¬P.IsEquipartition ↔ ∃ a ∈ P.parts, ∃ b ∈ P.parts, #b + 1 < #a

Tactic:
Set.not_equitableOn

Premises used: Set.not_equitableOn, Finpartition.IsEquipartition
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : (↑P.parts : Set (Finset α)).Subsingleton
⊢ P.IsEquipartition

Tactic:
Set.Subsingleton.equitableOn h _

Premises used: Set.Subsingleton.equitableOn, Finpartition.IsEquipartition
-- Module: Mathlib.Order.Partition.Equipartition
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

Tactic:
P.isEquipartition_iff_card_parts_eq_average.1 hP _ ht

Premises used: Finpartition.isEquipartition_iff_card_parts_eq_average, Iff.mp
-- Module: Mathlib.Order.Partition.Equipartition
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

Tactic:
have a := hP.card_parts_eq_average ht
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Tactic:
lia
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
rw : (∑ i ∈ P.parts, #i) / #P.parts ≤ #t
⊢ #s / #P.parts ≤ #t

Tactic:
rw [← P.sum_card_parts]

Premises used: Finpartition.sum_card_parts
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ (∑ i ∈ P.parts, #i) / #P.parts ≤ #t

Tactic:
Finset.EquitableOn.le hP ht

Premises used: Finset.EquitableOn.le
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ (∑ i ∈ P.parts, #i) / #P.parts ≤ #t

Tactic:
exact Finset.EquitableOn.le hP ht

Premises used: Finset.EquitableOn.le
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
rw : #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1
⊢ #t ≤ #s / #P.parts + 1

Tactic:
rw [← P.sum_card_parts]

Premises used: Finpartition.sum_card_parts
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1

Tactic:
Finset.EquitableOn.le_add_one hP ht

Premises used: Finset.EquitableOn.le_add_one
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1

Tactic:
exact Finset.EquitableOn.le_add_one hP ht

Premises used: Finset.EquitableOn.le_add_one
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
h : ∀ (p : Finset α), p ∈ {p ∈ P.parts | ¬#p = #s / #P.parts + 1} ↔ p ∈ {p ∈ P.parts | #p = #s / #P.parts}
⊢ {p ∈ P.parts | ¬#p = #s / #P.parts + 1} = {p ∈ P.parts | #p = #s / #P.parts}

Tactic:
ext p
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
h : p ∈ P.parts → (¬#p = #s / #P.parts + 1 ↔ #p = #s / #P.parts)
⊢ p ∈ {p ∈ P.parts | ¬#p = #s / #P.parts + 1} ↔ p ∈ {p ∈ P.parts | #p = #s / #P.parts}

Tactic:
simp only [mem_filter, and_congr_right_iff]

Premises used: and_congr_right_iff, Finset.mem_filter
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
⊢ p ∈ P.parts → (¬#p = #s / #P.parts + 1 ↔ #p = #s / #P.parts)

Tactic:
fun hp ↦ (hP.card_part_eq_average_iff hp).symm

Premises used: Finpartition.IsEquipartition.card_part_eq_average_iff, Iff.symm
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
⊢ p ∈ P.parts → (¬#p = #s / #P.parts + 1 ↔ #p = #s / #P.parts)

Tactic:
exact fun hp ↦ (hP.card_part_eq_average_iff hp).symm

Premises used: Finpartition.IsEquipartition.card_part_eq_average_iff, Iff.symm
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ ∑ i ∈ P.parts, #i = #s

Tactic:
have z := P.sum_card_parts
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : HAdd.hAdd (α := ℕ) (∑ x ∈ P.parts with #x = #s / #P.parts + 1, #x) (∑ x ∈ P.parts with #x = #s / #P.parts, #x) = #s
⊢ ∀ x ∈ {x ∈ P.parts | #x = #s / #P.parts + 1}, #x = #s / #P.parts + 1

Tactic:
simp
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) * (#s / #P.parts + 1) + ∑ x ∈ P.parts with #x = #s / #P.parts, #x = #s
⊢ ∀ x ∈ {p ∈ P.parts | #p = #s / #P.parts}, #x = #s / #P.parts

Tactic:
simp
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : ∑ i ∈ P.parts, #i = #s
⊢ #({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

Premises used: add_mul, Finpartition.IsEquipartition.filter_ne_average_add_one_eq_average, add_assoc, HDiv.hDiv, Finset.sum_const_nat, Finpartition.parts, add_comm, Finset.card_filter_add_card_filter_not, HAdd.hAdd, Finset.sum_filter_add_sum_filter_not, Finset.card, mul_add, mul_one, OfNat.ofNat, Eq
-- Module: Mathlib.Order.Partition.Equipartition
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
rw₂ rw₃ : #s = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts

Tactic:
rw [← add_left_inj, Nat.mod_add_div, z]

Premises used: add_left_inj, Nat.mod_add_div
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
arg : #P.parts
| #P.parts - #s % #P.parts

Tactic:
arg 1
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
rw : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1})
| #P.parts

Tactic:
rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]

Premises used: HDiv.hDiv, Finpartition.parts, Finset.card_filter_add_card_filter_not, HAdd.hAdd, Finset.card, OfNat.ofNat, Eq
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
arg : #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1})
| #P.parts - #s % #P.parts

Tactic:
arg 1
    rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]

Premises used: HDiv.hDiv, Finpartition.parts, Finset.card_filter_add_card_filter_not, HAdd.hAdd, Finset.card, OfNat.ofNat, Eq
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
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
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) = #P.parts - #s % #P.parts

Tactic:
conv_rhs =>
    arg 1
    rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]

Premises used: HDiv.hDiv, Finpartition.parts, Finset.card_filter_add_card_filter_not, HAdd.hAdd, Finset.card, OfNat.ofNat, Eq
-- Module: Mathlib.Order.Partition.Equipartition
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})
rw₂ rw₃ : #({p ∈ P.parts | #p = #s / #P.parts}) = #({p ∈ P.parts | #p = #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

Tactic:
rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]

Premises used: Finpartition.IsEquipartition.filter_ne_average_add_one_eq_average, Finpartition.IsEquipartition.card_large_parts_eq_mod, add_tsub_cancel_left