awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
n₁ n₂ : ℕ
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
rcases : ∀ (m : ℕ) (h₂ : enumerate sel s (n₁ + m) = some a) (hn : n₁ ≤ n₁ + m), n₁ = n₁ + m
⊢ n₁ = n₂

Tactic:
rcases Nat.le.dest hn with ⟨m, rfl⟩

Premises used: Nat.le.dest, rfl
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
h₂ : enumerate sel s (HAdd.hAdd (α := ℕ) 0 0) = some a
⊢ 0 = HAdd.hAdd (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
⊢ sel s = some a

Tactic:
simp_all only [enumerate, Nat.add_eq, zero_add]

Premises used: Nat.add_eq, zero_add, Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h₃ : sel s = some a
⊢ (do
      let a ← some a
      enumerate sel (s \ {a}) m) =
    some a

Tactic:
simp_all only [enumerate, Nat.add_eq, zero_add]

Premises used: Nat.add_eq, zero_add, Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
m : ℕ
h₁ : sel s = some a
h₂ :
  (do
      let a ← some a
      enumerate sel (s \ {a}) m) =
    some a
⊢ enumerate sel (s \ {a}) m = some a

Tactic:
h₂
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
m : ℕ
h₁ : sel s = some a
h₂ :
  (do
      let a ← some a
      enumerate sel (s \ {a}) m) =
    some a
⊢ enumerate sel (s \ {a}) m = some a

Tactic:
exact h₂
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
⊢ enumerate sel (s \ {a}) m = some a

Tactic:
have h' : enumerate sel (s \ {a}) m = some a := by
        simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ a ∈ s \ {a}

Tactic:
have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ 0 = 0 + (m + 1)

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s 0 = some a
h₂ : enumerate sel s (0 + m) = some a
zero : ∀ (h₂ : enumerate sel s (HAdd.hAdd (α := ℕ) 0 0) = some a), 0 = HAdd.hAdd (α := ℕ) 0 0
zero₁ : ∀ (m : ℕ) (h₂ : enumerate sel s (0 + (m + 1)) = some a), 0 = 0 + (m + 1)
⊢ 0 = 0 + m

Tactic:
cases m with
    | zero => rfl
    | succ m =>
      have h' : enumerate sel (s \ {a}) m = some a := by
        simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
      have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
      simp_all
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + 1 + m) = some a
⊢ k + 1 + m = k + m + 1

Tactic:
lia
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + 1 + m) = some a
⊢ enumerate sel s (k + m + 1) = some a

Tactic:
rw [show k + 1 + m = (k + m) + 1 by lia] at h₂
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + m + 1) = some a
succ : ∀ (h : sel s = none), k + 1 = k + 1 + m
succ₁ : ∀ (val : α) (h : sel s = some val), k + 1 = k + 1 + m
⊢ k + 1 = k + 1 + m

Tactic:
cases h : sel s
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + m + 1) = some a
h : sel s = none
⊢ k + 1 = k + 1 + m

Tactic:
simp_all [enumerate]

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + m + 1) = some a
val : α
h : sel s = some val
succ :
  ∀ (ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), m = 0)
    (h₁ : enumerate sel (s \ {val}) k = some a) (h₂ : enumerate sel (s \ {val}) (k + m) = some a)
    (h : sel s = some val), m = 0
⊢ k + 1 = k + 1 + m

Tactic:
simp_all [enumerate]

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
s : Set α
val : α
ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), m = 0
h₁ : enumerate sel (s \ {val}) k = some a
h₂ : enumerate sel (s \ {val}) (k + m) = some a
h : sel s = some val
⊢ m = 0

Tactic:
tauto
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
n₁ : ℕ
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
zero : ∀ {s : Set α} (h₁ : enumerate sel s 0 = some a) (h₂ : enumerate sel s (0 + m) = some a), 0 = 0 + m
succ :
  ∀ (k : ℕ) (ih : ∀ {s : Set α} (h₁ : enumerate sel s k = some a) (h₂ : enumerate sel s (k + m) = some a), k = k + m)
    {s : Set α} (h₁ : enumerate sel s (k + 1) = some a) (h₂ : enumerate sel s (k + 1 + m) = some a), k + 1 = k + 1 + m
⊢ n₁ = n₁ + m

Tactic:
induction n₁ generalizing s with
  | zero =>
    cases m with
    | zero => rfl
    | succ m =>
      have h' : enumerate sel (s \ {a}) m = some a := by
        simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
      have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
      simp_all
  | succ k ih =>
    rw [show k + 1 + m = (k + m) + 1 by lia] at h₂
    cases h : sel s <;> simp_all [enumerate]; tauto

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
β : Type u_2
inst : LE β
inst_1 : Add β
inst_2 : One β
f : α → β
⊢ EquitableOn ∅ f

Tactic:
fun a _ ha =>
  (Set.notMem_empty a ha).elim

Premises used: Set.EquitableOn, False.elim, Set.notMem_empty
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
h : ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
grw : b + 1 ≤ f y + 1
grw₁ grw₂ : f y + 1 ≤ f y + 1
⊢ f x ≤ f y + 1

Tactic:
grw [(hb x hx).2, (hb y hy).1]

Premises used: And.right, And.left
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
refine : s.EquitableOn f → ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ s.EquitableOn f ↔ ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
refine ⟨?_, fun ⟨b, hb⟩ x y hx hy => by grw [(hb x hx).2, (hb y hy).1]⟩
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
inl : EquitableOn ∅ f → ∃ (b : ℕ), ∀ (a : α), Membership.mem (γ := Set α) ∅ a → b ≤ f a ∧ f a ≤ b + 1
inr : ∀ (x : α) (hx : x ∈ s), s.EquitableOn f → ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ s.EquitableOn f → ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

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

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
f : α → ℕ
⊢ EquitableOn ∅ f → ∃ (b : ℕ), ∀ (a : α), Membership.mem (γ := Set α) ∅ a → b ≤ f a ∧ f a ≤ b + 1

Tactic:
simp
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
pos : ∀ (h : ∀ y ∈ s, f x ≤ f y), ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
neg : ∀ (h : ∃ y ∈ s, f y < f x), ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
by_cases! h : ∀ y ∈ s, f x ≤ f y
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : 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:
⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : 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⟩⟩
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
h : ∃ y ∈ s, f y < f x
neg : ∀ (w : α) (hw : w ∈ s) (hwx : f w < f x), ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
obtain ⟨w, hw, hwx⟩ := h
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : 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:
⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ ?_, hs hy hw⟩⟩

Premises used: Nat.le_of_succ_le_succ, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
neg : ∀ (y : α) (hy : y ∈ s), (f w).succ ≤ (f y).succ
⊢ ∃ (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⟩⟩
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : 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
neg : f x ≤ (f y).succ
⊢ (f w).succ ≤ (f y).succ

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

Premises used: Nat.succ_le_of_lt, LE.le.antisymm
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : 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:
hs hx hy
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : 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
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ (b : ℕ), f '' s ⊆ Icc b (b + 1)

Tactic:
simpa only [image_subset_iff] using equitableOn_iff_exists_le_le_add_one

Premises used: Set.equitableOn_iff_exists_le_le_add_one, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Set α
f : α → ℕ
simp_rw : (∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∃ (b : ℕ), ∀ a ∈ s, f a = b ∨ f a = b + 1
⊢ s.EquitableOn f ↔ ∃ (b : ℕ), ∀ a ∈ s, f a = b ∨ f a = b + 1

Tactic:
simp_rw [equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff]

Premises used: Set.equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
inst_1 : Add β
inst_2 : One β
s : Set α
f : α → β
⊢ ¬s.EquitableOn f ↔ ∃ a ∈ s, ∃ b ∈ s, f b + 1 < f a

Tactic:
simp [EquitableOn]

Premises used: Set.EquitableOn
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
β : Type u_2
inst : Semiring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
rw : f j ≤ f j + 1
⊢ f i ≤ f j + 1

Tactic:
rw [hs hi hj]
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
β : Type u_2
inst : Semiring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1

Tactic:
le_add_of_nonneg_right zero_le_one

Premises used: zero_le_one, le_add_of_nonneg_right
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
β : Type u_2
inst : Semiring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1

Tactic:
exact le_add_of_nonneg_right zero_le_one

Premises used: zero_le_one, le_add_of_nonneg_right
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
β : Type u_2
inst : Semiring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
a : α
f : α → β
⊢ EquitableOn {a} f

Tactic:
Set.subsingleton_singleton.equitableOn f

Premises used: Set.subsingleton_singleton, Set.Subsingleton.equitableOn
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
rw :
  (∃ (b : ℕ), ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1) ↔
    ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
⊢ (↑s : Set α).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
rw [Set.equitableOn_iff_exists_le_le_add_one]

Premises used: Set.equitableOn_iff_exists_le_le_add_one
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∃ (b : ℕ), ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1) ↔
    ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
⟨?_, fun h => ⟨_, h⟩⟩

Premises used: HDiv.hDiv, Iff.intro, Exists.intro, Finset.card, Finset.sum
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
refine :
  (∃ (b : ℕ), ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1) →
    ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
⊢ (∃ (b : ℕ), ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1) ↔
    ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
refine ⟨?_, fun h => ⟨_, h⟩⟩
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
pos : ∀ (h : ∀ a ∈ s, f a = b + 1), ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
neg : ∀ (h : ∃ a ∈ s, f a ≠ b + 1), ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
by_cases! h : ∀ a ∈ s, f a = b + 1
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
pos : b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1
⊢ (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]

Premises used: Iff.mpr, Nat.mul_div_cancel_left, Finset.sum_const_nat, Exists.intro, Finset.card_pos
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1

Tactic:
⟨le_rfl, Nat.le_succ _⟩

Premises used: le_rfl, Nat.le_succ, And.intro
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1

Tactic:
exact ⟨le_rfl, Nat.le_succ _⟩
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
h : ∃ a ∈ s, f a ≠ b + 1
neg : ∀ (x : α) (hx₁ : x ∈ s) (hx₂ : f x ≠ b + 1), ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := h
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i ∈ s, f i) / #s
simp_rw : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
simp_rw [← h]
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i ∈ s, f i) / #s
⊢ ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
apply hb
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
neg : b = (∑ i ∈ s, f i) / #s
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
suffices h : b = (∑ i ∈ s, f i) / s.card by
    simp_rw [← h]
    apply hb
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
neg : (∑ i ∈ s, f i) / #s = b
⊢ b = (∑ i ∈ s, f i) / #s

Tactic:
symm
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ b * #s ≤ ∑ i ∈ s, b

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
neg : ∑ i ∈ s, (b + 1) ≤ (b + 1) * #s
⊢ (∑ i ∈ s, f i) / #s = b

Tactic:
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 ?_)

Premises used: Nat.div_eq_of_lt_le, LE.le.lt_of_ne, And.right, And.left, LT.lt.trans_le, And.intro, Exists.intro, Finset.sum_le_sum, Finset.sum_lt_sum, le_trans
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
neg : ∀ x ∈ s, b + 1 = b + 1
⊢ ∑ i ∈ s, (b + 1) ≤ (b + 1) * #s

Tactic:
rw [mul_comm, sum_const_nat]

Premises used: Finset.sum_const_nat, mul_comm
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ x ∈ s, b + 1 = b + 1

Tactic:
fun _ _ => rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ (↑s : Set α), b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ x ∈ s, b + 1 = b + 1

Tactic:
exact fun _ _ => rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
h : (↑s : Set α).EquitableOn f
ha : a ∈ s
⊢ (∑ i ∈ s, f i) / #s ≤ f a

Tactic:
(equitableOn_iff_le_le_add_one.1 h a ha).1

Premises used: Finset.equitableOn_iff_le_le_add_one, And.left, Iff.mp
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
h : (↑s : Set α).EquitableOn f
ha : a ∈ s
⊢ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
(equitableOn_iff_le_le_add_one.1 h a ha).2

Premises used: Finset.equitableOn_iff_le_le_add_one, And.right, Iff.mp
-- Module: Mathlib.Data.Set.Equitable
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
simp_rw :
  (∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1) ↔
    ∀ a ∈ s, f a = (∑ i ∈ s, f i) / #s ∨ f a = (∑ i ∈ s, f i) / #s + 1
⊢ (↑s : Set α).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / #s ∨ f a = (∑ i ∈ s, f i) / #s + 1

Tactic:
simp_rw [equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff]

Premises used: Finset.equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
⊢ s.Finite ↔ Nonempty.{u + 1} (Fintype (↑s : Type u))

Tactic:
finite_iff_nonempty_fintype s

Premises used: Set.Finite, Set.Elem, finite_iff_nonempty_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
⊢ p.Finite

Tactic:
have := Fintype.ofFinset s H; p.toFinite

Premises used: Fintype.ofFinset, Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : Fintype (↑s : Type u)
h : s.Finite
rw : s.toFinset = s.toFinset
rw₁ : s.toFinset = s.toFinset
rw₂ : Fintype (↑s : Type u)
rw₃ : s.toFinset = s.toFinset
rw₄ : Fintype (↑s : Type u)
⊢ h.toFinset (s := s) = s.toFinset

Tactic:
rw [Finite.toFinset, Subsingleton.elim h.fintype]

Premises used: Set.Finite.fintype, Set.Finite.toFinset, Subsingleton.elim
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : Fintype (↑s : Type u)
⊢ ⋯.toFinset (s := s) = s.toFinset

Tactic:
s.toFinite.toFinset_eq_toFinset

Premises used: Set.Finite.toFinset_eq_toFinset, Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
intro : ∀ (val : Fintype (↑s : Type u)), ∃ (s' : Finset α), ∀ (a : α), a ∈ s' ↔ a ∈ s
⊢ ∃ (s' : Finset α), ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
cases h.nonempty_fintype

Premises used: Set.Finite.nonempty_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
val : Fintype (↑s : Type u)
⊢ ∃ (s' : Finset α), ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
⟨s.toFinset, fun _ => mem_toFinset⟩

Premises used: Set.toFinset, Exists.intro, Set.mem_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
val : Fintype (↑s : Type u)
⊢ ∃ (s' : Finset α), ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
exact ⟨s.toFinset, fun _ => mem_toFinset⟩
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
intro : ∀ (val : Fintype (↑s : Type u)), ∃ (s' : Finset α), (↑s' : Set α) = s
⊢ ∃ (s' : Finset α), (↑s' : Set α) = s

Tactic:
cases h.nonempty_fintype

Premises used: Set.Finite.nonempty_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
val : Fintype (↑s : Type u)
⊢ ∃ (s' : Finset α), (↑s' : Set α) = s

Tactic:
⟨s.toFinset, s.coe_toFinset⟩

Premises used: Set.toFinset, Exists.intro, Set.coe_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
val : Fintype (↑s : Type u)
⊢ ∃ (s' : Finset α), (↑s' : Set α) = s

Tactic:
exact ⟨s.toFinset, s.coe_toFinset⟩
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
a : α
hs : s.Finite
⊢ a ∈ hs.toFinset (s := s) ↔ a ∈ s

Tactic:
@mem_toFinset _ _ hs.fintype _

Premises used: Set.Mem, setOf, Set.mem_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
⊢ (↑(hs.toFinset (s := s)) : Set α) = s

Tactic:
@coe_toFinset _ _ hs.fintype

Premises used: setOf, Set.coe_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
rw : (↑(hs.toFinset (s := s)) : Set α).Nonempty ↔ s.Nonempty
rw₁ rw₂ : s.Nonempty ↔ s.Nonempty
⊢ hs.toFinset (s := s).Nonempty ↔ s.Nonempty

Tactic:
rw [← Finset.coe_nonempty, Finite.coe_toFinset]

Premises used: Finset.coe_nonempty, Set.Finite.coe_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
rw : (↑(↑(hs.toFinset (s := s)) : Set α) : Type u) = (↑s : Type u)
rw₁ rw₂ : (↑s : Type u) = (↑s : Type u)
⊢ ↥(hs.toFinset (s := s)) = (↑s : Type u)

Tactic:
rw [← Finset.coe_sort_coe _, hs.coe_toFinset]

Premises used: Finset.coe_sort_coe, Set.Finite.coe_toFinset