[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
obtain rfl | m_pos := m.eq_zero_or_pos
[GOAL]
case inl
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = card s
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = 0 ∨ card x = 0 + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ 0) ∧
        card (filter (fun i => card i = 0 + 1) Q.parts) = b
[PROOFSTEP]
refine' ⟨⊥, by simp, _, by simpa using hs.symm⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = card s
⊢ ∀ (x : Finset α), x ∈ ⊥.parts → card x = 0 ∨ card x = 0 + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = card s
⊢ card (filter (fun i => card i = 0 + 1) ⊥.parts) = b
[PROOFSTEP]
simpa using hs.symm
[GOAL]
case inl
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = card s
⊢ ∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) ⊥.parts) id) ≤ 0
[PROOFSTEP]
simp only [le_zero_iff, card_eq_zero, mem_biUnion, exists_prop, mem_filter, id.def, and_assoc,
  sdiff_eq_empty_iff_subset, subset_iff]
[GOAL]
case inl
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = card s
⊢ ∀ (x : Finset α), x ∈ P.parts → ∀ ⦃x_1 : α⦄, x_1 ∈ x → ∃ a, a ∈ ⊥.parts ∧ (∀ ⦃x_2 : α⦄, x_2 ∈ a → x_2 ∈ x) ∧ x_1 ∈ a
[PROOFSTEP]
exact fun x hx a ha =>
  ⟨{ a }, mem_map_of_mem _ (P.le hx ha), singleton_subset_iff.2 ha, mem_singleton_self _⟩
    -- Prove the case `m > 0` by strong induction on `s`
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
m_pos : m > 0
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
induction' s using Finset.strongInduction with s ih generalizing a b
[GOAL]
case inr.H
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
by_cases hab : a = 0 ∧ b = 0
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : a = 0 ∧ b = 0
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
simp only [hab.1, hab.2, add_zero, zero_mul, eq_comm, card_eq_zero, Finset.bot_eq_empty] at hs 
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hab : a = 0 ∧ b = 0
hs : s = ∅
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
subst hs
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s
hs : a✝ * m + b✝ * (m + 1) = card s
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ (t : Finset α),
    t ⊂ ∅ →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
P : Finpartition ∅
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
have : P = Finpartition.empty _ := Unique.eq_default (α := Finpartition ⊥) P
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s
hs : a✝ * m + b✝ * (m + 1) = card s
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ (t : Finset α),
    t ⊂ ∅ →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
P : Finpartition ∅
this : P = Finpartition.empty (Finset α)
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
exact ⟨Finpartition.empty _, by simp, by simp [this], by simp [hab.2]⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s
hs : a✝ * m + b✝ * (m + 1) = card s
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ (t : Finset α),
    t ⊂ ∅ →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
P : Finpartition ∅
this : P = Finpartition.empty (Finset α)
⊢ ∀ (x : Finset α), x ∈ (Finpartition.empty (Finset α)).parts → card x = m ∨ card x = m + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s
hs : a✝ * m + b✝ * (m + 1) = card s
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ (t : Finset α),
    t ⊂ ∅ →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
P : Finpartition ∅
this : P = Finpartition.empty (Finset α)
⊢ ∀ (x : Finset α),
    x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) (Finpartition.empty (Finset α)).parts) id) ≤ m
[PROOFSTEP]
simp [this]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s
hs : a✝ * m + b✝ * (m + 1) = card s
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ (t : Finset α),
    t ⊂ ∅ →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
P : Finpartition ∅
this : P = Finpartition.empty (Finset α)
⊢ card (filter (fun i => card i = m + 1) (Finpartition.empty (Finset α)).parts) = b
[PROOFSTEP]
simp [hab.2]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : ¬(a = 0 ∧ b = 0)
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
simp_rw [not_and_or, ← Ne.def, ← pos_iff_ne_zero] at hab 
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
set n := if 0 < a then m else m + 1 with hn
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
obtain ⟨hn₀, hn₁, hn₂, hn₃⟩ :
  0 < n ∧
    n ≤ m + 1 ∧ n ≤ a * m + b * (m + 1) ∧ ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = s.card - n :=
  by
  rw [hn, ← hs]
  split_ifs with h <;> rw [tsub_mul, one_mul]
  · refine' ⟨m_pos, le_succ _, le_add_right (le_mul_of_pos_left ‹0 < a›), _⟩
    rw [tsub_add_eq_add_tsub (le_mul_of_pos_left h)]
  · refine' ⟨succ_pos', le_rfl, le_add_left (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›), _⟩
    rw [← add_tsub_assoc_of_le (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›)]
      /- We will call the inductive hypothesis on a partition of `s \ t` for a carefully chosen `t ⊆ s`.
          To decide which, however, we must distinguish the case where all parts of `P` have size `m` (in
          which case we take `t` to be an arbitrary subset of `s` of size `n`) from the case where at
          least one part `u` of `P` has size `m + 1` (in which case we take `t` to be an arbitrary subset
          of `u` of size `n`). The rest of each branch is just tedious calculations to satisfy the
          induction hypothesis. -/
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
⊢ 0 < n ∧
    n ≤ m + 1 ∧
      n ≤ a * m + b * (m + 1) ∧ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
[PROOFSTEP]
rw [hn, ← hs]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
⊢ (0 < if 0 < a then m else m + 1) ∧
    (if 0 < a then m else m + 1) ≤ m + 1 ∧
      (if 0 < a then m else m + 1) ≤ a * m + b * (m + 1) ∧
        (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) =
          a * m + b * (m + 1) - if 0 < a then m else m + 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ (a - 1) * m + b * (m + 1) = a * m + b * (m + 1) - m
[PROOFSTEP]
rw [tsub_mul, one_mul]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧ m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b - 1) * (m + 1) = a * m + b * (m + 1) - (m + 1)
[PROOFSTEP]
rw [tsub_mul, one_mul]
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ a * m - m + b * (m + 1) = a * m + b * (m + 1) - m
[PROOFSTEP]
refine' ⟨m_pos, le_succ _, le_add_right (le_mul_of_pos_left ‹0 < a›), _⟩
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ a * m - m + b * (m + 1) = a * m + b * (m + 1) - m
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (le_mul_of_pos_left h)]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧
    m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b * (m + 1) - (m + 1)) = a * m + b * (m + 1) - (m + 1)
[PROOFSTEP]
refine' ⟨succ_pos', le_rfl, le_add_left (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›), _⟩
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ a * m + (b * (m + 1) - (m + 1)) = a * m + b * (m + 1) - (m + 1)
[PROOFSTEP]
rw [← add_tsub_assoc_of_le (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›)]
  /- We will call the inductive hypothesis on a partition of `s \ t` for a carefully chosen `t ⊆ s`.
      To decide which, however, we must distinguish the case where all parts of `P` have size `m` (in
      which case we take `t` to be an arbitrary subset of `s` of size `n`) from the case where at
      least one part `u` of `P` has size `m + 1` (in which case we take `t` to be an arbitrary subset
      of `u` of size `n`). The rest of each branch is just tedious calculations to satisfy the
      induction hypothesis. -/
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
by_cases h : ∀ u ∈ P.parts, card u < m + 1
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
obtain ⟨t, hts, htn⟩ := exists_smaller_set s n (hn₂.trans_eq hs)
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
have ht : t.Nonempty := by rwa [← card_pos, htn]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
⊢ Finset.Nonempty t
[PROOFSTEP]
rwa [← card_pos, htn]
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = (s \ t).card := by
  rw [card_sdiff ‹t ⊆ s›, htn, hn₃]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
⊢ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
[PROOFSTEP]
rw [card_sdiff ‹t ⊆ s›, htn, hn₃]
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
obtain ⟨R, hR₁, _, hR₃⟩ :=
  @ih (s \ t) (sdiff_ssubset hts ‹t.Nonempty›) (if 0 < a then a - 1 else a) (if 0 < a then b else b - 1) (P.avoid t)
    hcard
[GOAL]
case pos.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
refine' ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel hts), _, _, _⟩
[GOAL]
case pos.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ ∀ (x : Finset α),
    x ∈ (extend R (_ : t ≠ ∅) (_ : Disjoint (s \ t) t) (_ : s \ t ⊔ t = s)).parts → card x = m ∨ card x = m + 1
[PROOFSTEP]
simp only [extend_parts, mem_insert, forall_eq_or_imp, and_iff_left hR₁, htn, hn]
[GOAL]
case pos.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ (if 0 < a then m else m + 1) = m ∨ (if 0 < a then m else m + 1) = m + 1
[PROOFSTEP]
exact ite_eq_or_eq _ _ _
[GOAL]
case pos.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ ∀ (x : Finset α),
    x ∈ P.parts →
      card
          (x \
            Finset.biUnion
              (filter (fun y => y ⊆ x) (extend R (_ : t ≠ ∅) (_ : Disjoint (s \ t) t) (_ : s \ t ⊔ t = s)).parts) id) ≤
        m
[PROOFSTEP]
exact fun x hx => (card_le_of_subset <| sdiff_subset _ _).trans (lt_succ_iff.1 <| h _ hx)
[GOAL]
case pos.intro.intro.intro.intro.intro.refine'_3
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card (filter (fun i => card i = m + 1) (extend R (_ : t ≠ ∅) (_ : Disjoint (s \ t) t) (_ : s \ t ⊔ t = s)).parts) = b
[PROOFSTEP]
simp_rw [extend_parts, filter_insert, htn, m.succ_ne_self.symm.ite_eq_right_iff]
[GOAL]
case pos.intro.intro.intro.intro.intro.refine'_3
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card
      (if ¬0 < a then insert t (filter (fun i => card i = m + 1) R.parts)
      else filter (fun i => card i = m + 1) R.parts) =
    b
[PROOFSTEP]
split_ifs with ha
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
ha : 0 < a
⊢ card (filter (fun i => card i = m + 1) R.parts) = b
[PROOFSTEP]
rw [hR₃, if_pos ha]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
ha : ¬0 < a
⊢ card (insert t (filter (fun i => card i = m + 1) R.parts)) = b
[PROOFSTEP]
rw [card_insert_of_not_mem, hR₃, if_neg ha, tsub_add_cancel_of_le]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
ha : ¬0 < a
⊢ 1 ≤ b
[PROOFSTEP]
exact hab.resolve_left ha
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
ha : ¬0 < a
⊢ ¬t ∈ filter (fun i => card i = m + 1) R.parts
[PROOFSTEP]
intro H
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∀ (u : Finset α), u ∈ P.parts → card u < m + 1
t : Finset α
hts : t ⊆ s
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
left✝ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
ha : ¬0 < a
H : t ∈ filter (fun i => card i = m + 1) R.parts
⊢ False
[PROOFSTEP]
exact ht.ne_empty (le_sdiff_iff.1 <| R.le <| filter_subset _ _ H)
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ¬∀ (u : Finset α), u ∈ P.parts → card u < m + 1
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
h : ∃ u, u ∈ P.parts ∧ m + 1 ≤ card u
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
obtain ⟨u, hu₁, hu₂⟩ := h
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
obtain ⟨t, htu, htn⟩ := exists_smaller_set _ _ (hn₁.trans hu₂)
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
have ht : t.Nonempty := by rwa [← card_pos, htn]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
⊢ Finset.Nonempty t
[PROOFSTEP]
rwa [← card_pos, htn]
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = (s \ t).card := by
  rw [card_sdiff (htu.trans <| P.le hu₁), htn, hn₃]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
⊢ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
[PROOFSTEP]
rw [card_sdiff (htu.trans <| P.le hu₁), htn, hn₃]
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
obtain ⟨R, hR₁, hR₂, hR₃⟩ :=
  @ih (s \ t) (sdiff_ssubset (htu.trans <| P.le hu₁) ht) (if 0 < a then a - 1 else a) (if 0 < a then b else b - 1)
    (P.avoid t) hcard
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ ∃ Q,
    (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
      (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
        card (filter (fun i => card i = m + 1) Q.parts) = b
[PROOFSTEP]
refine' ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel <| htu.trans <| P.le hu₁), _, _, _⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ ∀ (x : Finset α),
    x ∈ (extend R (_ : t ≠ ∅) (_ : Disjoint (s \ t) t) (_ : s \ t ⊔ t = s)).parts → card x = m ∨ card x = m + 1
[PROOFSTEP]
simp only [mem_insert, forall_eq_or_imp, extend_parts, and_iff_left hR₁, htn, hn]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ (if 0 < a then m else m + 1) = m ∨ (if 0 < a then m else m + 1) = m + 1
[PROOFSTEP]
exact ite_eq_or_eq _ _ _
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ ∀ (x : Finset α),
    x ∈ P.parts →
      card
          (x \
            Finset.biUnion
              (filter (fun y => y ⊆ x) (extend R (_ : t ≠ ∅) (_ : Disjoint (s \ t) t) (_ : s \ t ⊔ t = s)).parts) id) ≤
        m
[PROOFSTEP]
conv in _ ∈ _ => rw [← insert_erase hu₁]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
x : Finset α
| x ∈ P.parts
[PROOFSTEP]
rw [← insert_erase hu₁]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
x : Finset α
| x ∈ P.parts
[PROOFSTEP]
rw [← insert_erase hu₁]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
x : Finset α
| x ∈ P.parts
[PROOFSTEP]
rw [← insert_erase hu₁]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ ∀ (x : Finset α),
    x ∈ insert u (erase P.parts u) →
      card
          (x \
            Finset.biUnion
              (filter (fun y => y ⊆ x) (extend R (_ : t ≠ ∅) (_ : Disjoint (s \ t) t) (_ : s \ t ⊔ t = s)).parts) id) ≤
        m
[PROOFSTEP]
simp only [and_imp, mem_insert, forall_eq_or_imp, Ne.def, extend_parts]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card (u \ Finset.biUnion (filter (fun y => y ⊆ u) (insert t R.parts)) id) ≤ m ∧
    ∀ (a : Finset α),
      a ∈ erase P.parts u → card (a \ Finset.biUnion (filter (fun y => y ⊆ a) (insert t R.parts)) id) ≤ m
[PROOFSTEP]
refine' ⟨_, fun x hx => (card_le_of_subset _).trans <| hR₂ x _⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card (u \ Finset.biUnion (filter (fun y => y ⊆ u) (insert t R.parts)) id) ≤ m
[PROOFSTEP]
simp only [filter_insert, if_pos htu, biUnion_insert, mem_erase, id.def]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card (u \ (t ∪ Finset.biUnion (filter (fun y => y ⊆ u) R.parts) id)) ≤ m
[PROOFSTEP]
obtain rfl | hut := eq_or_ne u t
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1.inl
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
htu : u ⊆ u
htn : card u = n
ht : Finset.Nonempty u
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ u)
R : Finpartition (s \ u)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P u).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card (u \ (u ∪ Finset.biUnion (filter (fun y => y ⊆ u) R.parts) id)) ≤ m
[PROOFSTEP]
rw [sdiff_eq_empty_iff_subset.2 (subset_union_left _ _)]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1.inl
α : Type u_1
inst✝ : DecidableEq α
s✝ t : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
htu : u ⊆ u
htn : card u = n
ht : Finset.Nonempty u
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ u)
R : Finpartition (s \ u)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P u).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card ∅ ≤ m
[PROOFSTEP]
exact bot_le
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1.inr
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
hut : u ≠ t
⊢ card (u \ (t ∪ Finset.biUnion (filter (fun y => y ⊆ u) R.parts) id)) ≤ m
[PROOFSTEP]
refine'
  (card_le_of_subset fun i => _).trans
    (hR₂ (u \ t) <| P.mem_avoid.2 ⟨u, hu₁, fun i => hut <| i.antisymm htu, rfl⟩)
      -- Porting note: `not_and` required because `∃ x ∈ s, p x` is defined differently
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1.inr
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
hut : u ≠ t
i : α
⊢ i ∈ u \ (t ∪ Finset.biUnion (filter (fun y => y ⊆ u) R.parts) id) →
    i ∈ (u \ t) \ Finset.biUnion (filter (fun y => y ⊆ u \ t) R.parts) id
[PROOFSTEP]
simp only [not_exists, not_and, mem_biUnion, and_imp, mem_union, mem_filter, mem_sdiff, id.def, not_or]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1.inr
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
hut : u ≠ t
i : α
⊢ i ∈ u →
    ¬i ∈ t →
      (∀ (x : Finset α), x ∈ R.parts → x ⊆ u → ¬i ∈ x) →
        (i ∈ u ∧ ¬i ∈ t) ∧ ∀ (x : Finset α), x ∈ R.parts → x ⊆ u \ t → ¬i ∈ x
[PROOFSTEP]
exact fun hi₁ hi₂ hi₃ => ⟨⟨hi₁, hi₂⟩, fun x hx hx' => hi₃ _ hx <| hx'.trans <| sdiff_subset _ _⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
x : Finset α
hx : x ∈ erase P.parts u
⊢ x \ Finset.biUnion (filter (fun y => y ⊆ x) (insert t R.parts)) id ⊆
    x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id
[PROOFSTEP]
apply sdiff_subset_sdiff Subset.rfl (biUnion_subset_biUnion_of_subset_left _ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
x : Finset α
hx : x ∈ erase P.parts u
⊢ filter (fun y => y ⊆ x) R.parts ⊆ filter (fun y => y ⊆ x) (insert t R.parts)
[PROOFSTEP]
exact filter_subset_filter _ (subset_insert _ _)
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_3
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
x : Finset α
hx : x ∈ erase P.parts u
⊢ x ∈ (avoid P t).parts
[PROOFSTEP]
simp only [avoid, ofErase, mem_erase, mem_image, bot_eq_empty]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_3
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
x : Finset α
hx : x ∈ erase P.parts u
⊢ x ≠ ∅ ∧ ∃ a, a ∈ P.parts ∧ a \ t = x
[PROOFSTEP]
exact
  ⟨(nonempty_of_mem_parts _ <| mem_of_mem_erase hx).ne_empty, _, mem_of_mem_erase hx,
    (disjoint_of_subset_right htu <| P.disjoint (mem_of_mem_erase hx) hu₁ <| ne_of_mem_erase hx).sdiff_eq_left⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_3
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card (filter (fun i => card i = m + 1) (extend R (_ : t ≠ ∅) (_ : Disjoint (s \ t) t) (_ : s \ t ⊔ t = s)).parts) = b
[PROOFSTEP]
simp only [extend_parts, filter_insert, htn, hn, m.succ_ne_self.symm.ite_eq_right_iff]
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.refine'_3
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ card
      (if ¬0 < a then insert t (filter (fun i => card i = m + 1) R.parts)
      else filter (fun i => card i = m + 1) R.parts) =
    b
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
h : 0 < a
⊢ card (filter (fun i => card i = m + 1) R.parts) = b
[PROOFSTEP]
rw [hR₃, if_pos h]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
h : ¬0 < a
⊢ card (insert t (filter (fun i => card i = m + 1) R.parts)) = b
[PROOFSTEP]
rw [card_insert_of_not_mem, hR₃, if_neg h, Nat.sub_add_cancel (hab.resolve_left h)]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
h : ¬0 < a
⊢ ¬t ∈ filter (fun i => card i = m + 1) R.parts
[PROOFSTEP]
intro H
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
m n✝ a✝ b✝ : ℕ
P✝ : Finpartition s✝
hs✝ : a✝ * m + b✝ * (m + 1) = card s✝
m_pos : m > 0
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {a b : ℕ} {P : Finpartition t},
        a * m + b * (m + 1) = card t →
          ∃ Q,
            (∀ (x : Finset α), x ∈ Q.parts → card x = m ∨ card x = m + 1) ∧
              (∀ (x : Finset α), x ∈ P.parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧
                card (filter (fun i => card i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = card s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ card u
t : Finset α
htu : t ⊆ u
htn : card t = n
ht : Finset.Nonempty t
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = card (s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ (x : Finset α), x ∈ R.parts → card x = m ∨ card x = m + 1
hR₂ : ∀ (x : Finset α), x ∈ (avoid P t).parts → card (x \ Finset.biUnion (filter (fun y => y ⊆ x) R.parts) id) ≤ m
hR₃ : card (filter (fun i => card i = m + 1) R.parts) = if 0 < a then b else b - 1
h : ¬0 < a
H : t ∈ filter (fun i => card i = m + 1) R.parts
⊢ False
[PROOFSTEP]
exact ht.ne_empty (le_sdiff_iff.1 <| R.le <| filter_subset _ _ H)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) = a
[PROOFSTEP]
refine' (mul_eq_mul_right_iff.1 <| (add_left_inj (b * (m + 1))).1 _).resolve_right hm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) = a * m + b * (m + 1)
[PROOFSTEP]
rw [h, ← (P.equitabilise h).sum_card_parts]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum (equitabilise h).parts fun i => card i
[PROOFSTEP]
have hunion :
  (P.equitabilise h).parts =
    ((P.equitabilise h).parts.filter fun u => u.card = m) ∪ (P.equitabilise h).parts.filter fun u => u.card = m + 1 :=
  by
  rw [← filter_or, filter_true_of_mem]
  exact fun x => card_eq_of_mem_parts_equitabilise
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
[PROOFSTEP]
rw [← filter_or, filter_true_of_mem]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ ∀ (x : Finset α), x ∈ (equitabilise h).parts → card x = m ∨ card x = m + 1
[PROOFSTEP]
exact fun x => card_eq_of_mem_parts_equitabilise
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum (equitabilise h).parts fun i => card i
[PROOFSTEP]
nth_rw 2 [hunion]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum
      (filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts)
      fun i => card i
[PROOFSTEP]
rw [sum_union, sum_const_nat fun x hx => (mem_filter.1 hx).2, sum_const_nat fun x hx => (mem_filter.1 hx).2,
  P.card_filter_equitabilise_big]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ Disjoint (filter (fun u => card u = m) (equitabilise h).parts)
    (filter (fun u => card u = m + 1) (equitabilise h).parts)
[PROOFSTEP]
refine' disjoint_filter_filter' _ _ _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ Disjoint (fun u => card u = m) fun u => card u = m + 1
[PROOFSTEP]
intro x ha hb i h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => card u = m) (equitabilise h✝).parts ∪ filter (fun u => card u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => card u = m
hb : x ≤ fun u => card u = m + 1
i : Finset α
h : x i
⊢ ⊥ i
[PROOFSTEP]
apply succ_ne_self m _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => card u = m) (equitabilise h✝).parts ∪ filter (fun u => card u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => card u = m
hb : x ≤ fun u => card u = m + 1
i : Finset α
h : x i
⊢ succ m = m
[PROOFSTEP]
exact (hb i h).symm.trans (ha i h)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (equitabilise h).parts = a + b
[PROOFSTEP]
rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or, card_union_eq,
  P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]
  -- Porting note: was `infer_instance`
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ Disjoint (filter (fun x => card x = m) (equitabilise h).parts)
    (filter (fun x => card x = m + 1) (equitabilise h).parts)
[PROOFSTEP]
exact disjoint_filter.2 fun x _ h₀ h₁ => Nat.succ_ne_self m <| h₁.symm.trans h₀
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : n ≠ 0
hs : n ≤ card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
[PROOFSTEP]
rw [← pos_iff_ne_zero] at hn 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
[PROOFSTEP]
have : (n - s.card % n) * (s.card / n) + s.card % n * (s.card / n + 1) = s.card := by
  rw [tsub_mul, mul_add, ← add_assoc, tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one,
    add_comm, mod_add_div]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
⊢ (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
[PROOFSTEP]
rw [tsub_mul, mul_add, ← add_assoc, tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
  mod_add_div]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
this : (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
[PROOFSTEP]
refine' ⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this, equitabilise_isEquipartition, _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
this : (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
⊢ card (equitabilise this).parts = n
[PROOFSTEP]
rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]
