-- Mathlib/Data/Set/Equitable.lean
theorem equitableOn_iff_exists_le_le_add_one {s : Set α} {f : α → ℕ} :
    s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Proof state:
case neg.intro.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
refine ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ ?_, hs hy hw⟩⟩

Result:
case neg.intro.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ (f w).succ ≤ (f y).succ

Proof state:
case inl
α : Type u_1
f : α → ℕ
⊢ ∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∃ y ∈ s, f y < f x
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
obtain ⟨w, hw, hwx⟩ := h

Result:
case neg.intro.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Proof state:
case inr.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
intro hs

Result:
case inr.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Proof state:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
refine ⟨?_, fun ⟨b, hb⟩ x y hx hy => (hb x hx).2.trans (add_le_add_right (hb y hy).1 _)⟩

Result:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Proof state:
case inr.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
by_cases h : ∀ y ∈ s, f x ≤ f y

Result:
case pos
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∀ y ∈ s, f x ≤ f y
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ¬∀ y ∈ s, f x ≤ f y
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Proof state:
case pos
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∀ y ∈ s, f x ≤ f y
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩

Result:
no goals

Proof state:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_1
f : α → ℕ
⊢ ∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1

case inr.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Proof state:
case neg.intro.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ (f w).succ ≤ (f y).succ

Tactic:
rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]

Result:
case neg.intro.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ f x ≤ (f y).succ

Proof state:
case neg.intro.intro
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ f x ≤ (f y).succ

Tactic:
exact hs hx hy

Result:
no goals

Proof state:
case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ¬∀ y ∈ s, f x ≤ f y
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
push_neg at h

Result:
case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∃ y ∈ s, f y < f x
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1