α : Type u_1
β : Type ?u.456
s : Set α
f : α → ℕ
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
α : Type u_1
β : Type ?u.456
s : Set α
f : α → ℕ
⊢ EquitableOn s f ↔ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
refine' ⟨_, fun ⟨b, hb⟩ x y hx hy => (hb x hx).2.trans (add_le_add_right (hb y hy).1 _)⟩
case inl
α : Type u_1
β : Type ?u.456
f : α → ℕ
⊢ EquitableOn ∅ f → ∃ b, ∀ (a : α), a ∈ ∅ → b ≤ f a ∧ f a ≤ b + 1

case inr.intro
α : Type u_1
β : Type ?u.456
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
α : Type u_1
β : Type ?u.456
s : Set α
f : α → ℕ
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
case inr.intro
α : Type u_1
β : Type ?u.456
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
case inr.intro
α : Type u_1
β : Type ?u.456
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
intro hs
case pos
α : Type u_1
β : Type ?u.456
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

case neg
α : Type u_1
β : Type ?u.456
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
case inr.intro
α : Type u_1
β : Type ?u.456
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
by_cases h : ∀ y ∈ s, f x ≤ f y
case neg
α : Type u_1
β : Type ?u.456
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
case neg
α : Type u_1
β : Type ?u.456
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
push_neg at h
case neg.intro.intro
α : Type u_1
β : Type ?u.456
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
case neg
α : Type u_1
β : Type ?u.456
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
obtain ⟨w, hw, hwx⟩ := h
case neg.intro.intro
α : Type u_1
β : Type ?u.456
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)
case neg.intro.intro
α : Type u_1
β : Type ?u.456
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
refine' ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ _, hs hy hw⟩⟩
case neg.intro.intro
α : Type u_1
β : Type ?u.456
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)
case neg.intro.intro
α : Type u_1
β : Type ?u.456
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)
rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]
no goals
case neg.intro.intro
α : Type u_1
β : Type ?u.456
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)
exact hs hx hy
no goals
case inl
α : Type u_1
β : Type ?u.456
f : α → ℕ
⊢ EquitableOn ∅ f → ∃ b, ∀ (a : α), a ∈ ∅ → b ≤ f a ∧ f a ≤ b + 1
simp
no goals
case pos
α : Type u_1
β : Type ?u.456
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
exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩