α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
⊢ (∃ b, ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1) ↔
    ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
⊢ EquitableOn (↑s) f ↔ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
rw [Set.equitableOn_iff_exists_le_le_add_one]
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
⊢ (∃ b, ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1) →
    ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
⊢ (∃ b, ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1) ↔
    ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
refine' ⟨_, fun h => ⟨_, h⟩⟩
case intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
⊢ (∃ b, ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1) →
    ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
rintro ⟨b, hb⟩
case pos
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1

case neg
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ¬∀ (a : α), a ∈ s → f a = b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
case intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
by_cases h : ∀ a ∈ s, f a = b + 1
case neg
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∃ a, a ∈ s ∧ f a ≠ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
case neg
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ¬∀ (a : α), a ∈ s → f a = b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
push_neg at h
case neg.intro.intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
case neg
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∃ a, a ∈ s ∧ f a ≠ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
obtain ⟨x, hx₁, hx₂⟩ := h
case neg.intro.intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i in s, f i) / card s
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1

case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ b = (∑ i in s, f i) / card s
case neg.intro.intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
suffices h : b = (∑ i in s, f i) / s.card
case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ (∑ i in s, f i) / card s = b
case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ b = (∑ i in s, f i) / card s
symm
case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∑ i in s, (b + 1) ≤ Nat.succ b * card s
case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ (∑ i in s, f i) / card s = b
refine'
  Nat.div_eq_of_lt_le (le_trans (by simp [mul_comm]) (sum_le_sum fun a ha => (hb a ha).1))
    ((sum_lt_sum (fun a ha => (hb a ha).2) ⟨_, hx₁, (hb _ hx₁).2.lt_of_ne hx₂⟩).trans_le _)
case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ (x : α), x ∈ s → b + 1 = Nat.succ b
case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∑ i in s, (b + 1) ≤ Nat.succ b * card s
rw [mul_comm, sum_const_nat]
no goals
case h
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ (x : α), x ∈ s → b + 1 = Nat.succ b
exact fun _ _ => rfl
case pos
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a✝ : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
a : α
ha : a ∈ s
⊢ (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
case pos
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
intro a ha
case pos
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a✝ : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1
case pos
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a✝ : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
a : α
ha : a ∈ s
⊢ (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]
no goals
case pos
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a✝ : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1
exact ⟨le_rfl, Nat.le_succ _⟩
case neg.intro.intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i in s, f i) / card s
⊢ ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
case neg.intro.intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i in s, f i) / card s
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
simp_rw [← h]
no goals
case neg.intro.intro
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i in s, f i) / card s
⊢ ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
apply hb
no goals
α : Type u_1
β : Type ?u.8332
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ b * card s ≤ ∑ i in s, b
simp [mul_comm]