[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f ↔ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
refine' ⟨_, fun ⟨b, hb⟩ x y hx hy => (hb x hx).2.trans (add_le_add_right (hb y hy).1 _)⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
[GOAL]
case inl
α : Type u_1
β : Type u_2
f : α → ℕ
⊢ EquitableOn ∅ f → ∃ b, ∀ (a : α), a ∈ ∅ → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
simp
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
intro hs
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
by_cases h : ∀ y ∈ s, f x ≤ f y
[GOAL]
case pos
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
h : ∀ (y : α), y ∈ s → f x ≤ f y
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
h : ¬∀ (y : α), y ∈ s → f x ≤ f y
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
h : ∃ y, y ∈ s ∧ f y < f x
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
obtain ⟨w, hw, hwx⟩ := h
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
w : α
hw : w ∈ s
hwx : f w < f x
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
refine' ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ _, hs hy hw⟩⟩
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ Nat.succ (f w) ≤ Nat.succ (f y)
[PROOFSTEP]
rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ f x ≤ Nat.succ (f y)
[PROOFSTEP]
exact hs hx hy
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f ↔ ∃ b, f '' s ⊆ Icc b (b + 1)
[PROOFSTEP]
simpa only [image_subset_iff] using equitableOn_iff_exists_le_le_add_one
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f ↔ ∃ b, ∀ (a : α), a ∈ s → f a = b ∨ f a = b + 1
[PROOFSTEP]
simp_rw [equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : Set.Subsingleton s
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1
[PROOFSTEP]
rw [hs hi hj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : Set.Subsingleton s
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1
[PROOFSTEP]
exact le_add_of_nonneg_right zero_le_one
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [Set.equitableOn_iff_exists_le_le_add_one]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' ⟨_, fun h => ⟨_, h⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rintro ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
by_cases h : ∀ a ∈ s, f a = b + 1
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
intro a ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact ⟨le_rfl, Nat.le_succ _⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨x, hx₁, hx₂⟩ := h
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
suffices h : b = (∑ i in s, f i) / s.card
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp_rw [← h]
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply hb
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
symm
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
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 _)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [mul_comm, sum_const_nat]
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact fun _ _ => rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
⊢ EquitableOn (↑s) f ↔ ∀ (a : α), a ∈ s → f a = (∑ i in s, f i) / card s ∨ f a = (∑ i in s, f i) / card s + 1
[PROOFSTEP]
simp_rw [equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff]
