awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
⊢ Countable.{v + 1} (↑{t : β | (f t).Nonempty} : Type v)
have A : Injective F
Tactic: have A : Injective F := by
    rintro ⟨t, ht⟩ ⟨t', ht'⟩ htt'
    have A : (f t ∩ f t').Nonempty := by
      refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
      rw [htt']
      exact hF ⟨t', _⟩
    simp only [Subtype.mk.injEq]
    by_contra H
    exact not_disjoint_iff_nonempty_inter.2 A (hf H)
-- Lean 4 proof step from Mathlib.Data.Set.Disjoint (goal)
Goal:
α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
have rw : Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
Tactic: rw [disjoint_comm, disjoint_left]
-- Lean 4 proof step from Mathlib.Data.Set.Disjoint (goal)
Goal:
α : Type u
s t : Set α
rw : Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
have rw₁ : (∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s) ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
Tactic: rw [disjoint_comm, disjoint_left]
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ dissipate s n = ⋂ (k : ℕ), ⋂ (_ : k < n + 1), s k
have simp_rw : dissipate s n = ⋂ (k : ℕ), ⋂ (_ : k ≤ n), s k
Tactic: simp_rw [Nat.lt_add_one_iff, dissipate]
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
⊢ ⋂ (i : α), s i ⊆ dissipate s x
have simp : ∀ (i : α) (i_1 : i ≤ x), ⋂ (i : α), s i ⊆ s i
Tactic: simp only [dissipate, subset_iInter_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
⊢ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y = dissipate s x
have h₁ : ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
h₁ : ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x
⊢ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y = dissipate s x
have h₂ : dissipate s x ⊆ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
⊢ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x
have apply : ∀ (z : α) (y : β) (hy : Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), dissipate s z) y),
  Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), s z) y
Tactic: apply iInter_mono fun z y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x z : α
y : β
hy : Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), dissipate s z) y
⊢ Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), s z) y
have simp : ∀ (hy : ∀ (i : z ≤ x), ∀ y_1 ≤ z, y ∈ s y_1) (i : z ≤ x), y ∈ s z
Tactic: simp only [mem_iInter, mem_dissipate] at *
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
⊢ dissipate s x ⊆ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y
have h₂ : ∀ (i : α) (i_1 : i ≤ x), dissipate s x ⊆ dissipate s i
Tactic: simp only [subset_iInter_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)
have h₁ : Subset.{u_2} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
h₁ : Subset.{u_2} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)
have h₂ : Subset.{u_2} (α := Set β) (⋂ (x : α), s x) (⋂ (x : α), dissipate s x)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Subset.{u_2} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)
have h₁ : ∀ (x : β), (∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1) → ∀ (i : α), x ∈ s i
Tactic: simp_rw [subset_def, dissipate_def, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Subset.{u_2} (α := Set β) (⋂ (x : α), s x) (⋂ (x : α), dissipate s x)
have h₂ : ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1
Tactic: simp_rw [subset_def, dissipate_def, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
n : ℕ
⊢ dissipate s (n + 1) = dissipate s n ∩ s (n + 1)
have h : ∀ (x : α), x ∈ dissipate s (n + 1) ↔ x ∈ dissipate s n ∩ s (n + 1)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
n : ℕ
x : α
⊢ x ∈ dissipate s (n + 1) ↔ x ∈ dissipate s n ∩ s (n + 1)
have h : (∀ (i : ℕ) (i_1 : i ≤ n + 1), x ∈ s i) ↔ (∀ (i : ℕ) (i_1 : i ≤ n), x ∈ s i) ∧ x ∈ s (n + 1)
Tactic: simp_all only [dissipate_def, mem_iInter, mem_inter_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
⊢ ∃ (m : ℕ), s m ⊆ dissipate s 0
have h : s 0 ⊆ dissipate s 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n : ℕ
hn : ∃ (m : ℕ), s m ⊆ dissipate s n
⊢ ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)
have succ : ∀ (m : ℕ) (hm : s m ⊆ dissipate s n), ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)
Tactic: obtain ⟨m, hm⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n m : ℕ
hm : s m ⊆ dissipate s n
⊢ ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)
have succ : ∀ (k : ℕ) (hk : (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) (s m) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) (s (n + 1)) (s k)),
  ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)
Tactic: obtain ⟨k, hk⟩ := hd m (n + 1)
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n m : ℕ
hm : s m ⊆ dissipate s n
k : ℕ
hk : (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) (s m) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) (s (n + 1)) (s k)
⊢ s k ⊆ dissipate s (n + 1)
have simp : s k ⊆ dissipate s n ∧ s k ⊆ s (n + 1)
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n : ℕ
⊢ ∃ (m : ℕ), s m ⊆ dissipate s n
have zero : ∃ (m : ℕ), s m ⊆ dissipate s 0
Tactic: induction n with
  | zero => use 0; simp [dissipate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    exact ⟨k, by simp; grind⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n : ℕ
zero : ∃ (m : ℕ), s m ⊆ dissipate s 0
⊢ ∃ (m : ℕ), s m ⊆ dissipate s n
have succ : ∀ (n : ℕ) (hn : ∃ (m : ℕ), s m ⊆ dissipate s n), ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)
Tactic: induction n with
  | zero => use 0; simp [dissipate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    exact ⟨k, by simp; grind⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
⊢ (∃ (n : ℕ), dissipate s n = ∅) ↔ ∃ (n : ℕ), s n = ∅
have refine : (∃ (n : ℕ), dissipate s n = ∅) → ∃ (n : ℕ), s n = ∅
Tactic: refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
⊢ (∃ (n : ℕ), dissipate s n = ∅) → ∃ (n : ℕ), s n = ∅
have contrapose! : (∀ (n : ℕ), (s n).Nonempty) → ∀ (n : ℕ), (dissipate s n).Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Set.Dissipate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
h : ∀ (n : ℕ), (s n).Nonempty
n : ℕ
⊢ (dissipate s n).Nonempty
have obtain : ∀ (m : ℕ) (hm : s m ⊆ dissipate s n), (dissipate s n).Nonempty
Tactic: obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
⊢ enumerate sel s m = none
have none : ∀ (hs : sel s = none), enumerate sel s m = none
Tactic: cases hs : sel s
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = Option.none
hm : n + 1 ≤ m
none : ∀ (hs : sel s = Option.none), enumerate sel s m = Option.none
⊢ enumerate sel s m = Option.none
have some : ∀ (val : α) (hs : sel s = some val), enumerate sel s m = Option.none
Tactic: cases hs : sel s
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val : α
hs : sel s = some val
m' : ℕ
hm : n + 1 ≤ m' + 1
⊢ enumerate sel s (m' + 1) = none
have some : ∀
  (h :
    Eq (α := Option α)
      (do
        let a ← some val
        enumerate sel (s \ {a}) n)
      none),
  Eq (α := Option α)
    (do
      let a ← some val
      enumerate sel (s \ {a}) m')
    none
Tactic: simp only [enumerate, hs] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (hypothesis)
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val : α
hs : sel s = some val
m' : ℕ
hm : n + 1 ≤ m' + 1
h :
  Eq (α := Option α)
    (do
      let a ← some val
      enumerate sel (s \ {a}) n)
    none
⊢ Eq (α := Option α)
    (do
      let a ← some val
      enumerate sel (s \ {a}) m')
    none
have hm₁ : n ≤ m'
Tactic: have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
val : α
hs : sel s = some val
⊢ enumerate sel s m = none
have some : ∀ (hm : n + 1 ≤ 0), enumerate sel s 0 = none
Tactic: cases m with
      | zero => contradiction
      | succ m' =>
        simp only [enumerate, hs] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
val : α
hs : sel s = Option.some val
some : ∀ (hm : n + 1 ≤ 0), enumerate sel s 0 = none
⊢ enumerate sel s m = none
have some₁ : ∀ (m' : ℕ) (hm : n + 1 ≤ m' + 1), enumerate sel s (m' + 1) = none
Tactic: cases m with
      | zero => contradiction
      | succ m' =>
        simp only [enumerate, hs] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ enumerate sel s (n + 1) = some a → a ∈ s
have some : (do
      let a ← some a'
      enumerate sel (s \ {a}) n) =
    some a →
  a ∈ s
Tactic: simp only [enumerate, h]
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
⊢ enumerate sel s (n + 1) = some a → a ∈ s
have cases : ∀ (x : Option α) (h : sel s = x), enumerate sel s (n + 1) = some a → a ∈ s
Tactic: cases h : sel s with
    | none => simp [enumerate_eq_none_of_sel, h]
    | some a' =>
      simp only [enumerate, h]
      exact fun h' : enumerate sel (s \ {a'}) n = some a ↦
        have : a ∈ s \ {a'} := enumerate_mem h_sel h'
        this.left
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
⊢ n₁ = n₂
have inr : ∀ (this : ∀ {n₁ n₂ : ℕ} (h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) (hn : n₁ ≤ n₂), n₁ = n₂)
  (hn : n₂ < n₁), n₁ = n₂
Tactic: wlog! hn : n₁ ≤ n₂ generalizing n₁ n₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
Goal:
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
inr :
  ∀ (this : ∀ {n₁ n₂ : ℕ} (h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) (hn : n₁ ≤ n₂), n₁ = n₂)
    (hn : n₂ < n₁), n₁ = n₂
⊢ n₁ = n₂
have wlog! : ∀ {n₁ n₂ : ℕ} (h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) (hn : n₁ ≤ n₂), n₁ = n₂
Tactic: wlog! hn : n₁ ≤ n₂ generalizing n₁ n₂
Cleared hypotheses: n₁, n₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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₂
⊢ n₁ = n₂
have rcases : ∀ (m : ℕ) (h₂ : enumerate sel s (n₁ + m) = some a) (hn : n₁ ≤ n₁ + m), n₁ = n₁ + m
Tactic: rcases Nat.le.dest hn with ⟨m, rfl⟩
Cleared hypotheses: n₂, h₂, hn
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (hypothesis)
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
have h₃ : sel s = some a
Tactic: simp_all only [enumerate, Nat.add_eq, zero_add]
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (hypothesis)
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
⊢ enumerate sel (s \ {a}) m = some a
have h₄ : (do
    let a ← some a
    enumerate sel (s \ {a}) m) =
  some a
Tactic: simp_all only [enumerate, Nat.add_eq, zero_add]
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (hypothesis)
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
⊢ 0 = 0 + (m + 1)
have h' : 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₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (hypothesis)
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
⊢ 0 = 0 + (m + 1)
have this : a ∈ s \ {a}
Tactic: have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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
⊢ 0 = 0 + m
have zero : ∀ (h₂ : enumerate sel s (HAdd.hAdd (α := ℕ) 0 0) = some a), 0 = HAdd.hAdd (α := ℕ) 0 0
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
Cleared hypotheses: m, h₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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
⊢ 0 = 0 + m
have zero₁ : ∀ (m : ℕ) (h₂ : enumerate sel s (0 + (m + 1)) = some a), 0 = 0 + (m + 1)
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
Cleared hypotheses: m, h₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (hypothesis)
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 = k + 1 + m
have h₃ : enumerate sel s (k + m + 1) = some a
Tactic: rw [show k + 1 + m = (k + m) + 1 by lia] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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
⊢ k + 1 = k + 1 + m
have succ : ∀ (h : sel s = none), k + 1 = k + 1 + m
Tactic: cases h : sel s
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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
⊢ k + 1 = k + 1 + m
have succ₁ : ∀ (val : α) (h : sel s = some val), k + 1 = k + 1 + m
Tactic: cases h : sel s
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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
⊢ k + 1 = k + 1 + m
have 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
Tactic: simp_all [enumerate]
Cleared hypotheses: ih, h₁, h₂, h
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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
⊢ n₁ = n₁ + m
have zero : ∀ {s : Set α} (h₁ : enumerate sel s 0 = some a) (h₂ : enumerate sel s (0 + m) = some a), 0 = 0 + 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
Cleared hypotheses: s, n₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Set.Enumerate (goal)
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
⊢ n₁ = n₁ + m
have 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
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
Cleared hypotheses: s, n₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
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
⊢ f x ≤ f y + 1
have grw : b + 1 ≤ f y + 1
Tactic: grw [(hb x hx).2, (hb y hy).1]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
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
⊢ f x ≤ f y + 1
have grw₁ : f y + 1 ≤ f y + 1
Tactic: grw [(hb x hx).2, (hb y hy).1]
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
have refine : 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]⟩
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f → ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
have inl : EquitableOn ∅ f → ∃ (b : ℕ), ∀ (a : α), Membership.mem (γ := Set α) ∅ a → b ≤ f a ∧ f a ≤ b + 1
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Set α
f : α → ℕ
inl : EquitableOn ∅ f → ∃ (b : ℕ), ∀ (a : α), Membership.mem (γ := Set α) ∅ a → b ≤ f a ∧ f a ≤ b + 1
⊢ s.EquitableOn f → ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
have inr : ∀ (x : α) (hx : x ∈ s), s.EquitableOn f → ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
⊢ ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
have pos : ∀ (h : ∀ y ∈ s, f x ≤ f y), ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Tactic: by_cases! h : ∀ y ∈ s, f x ≤ f y
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
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
⊢ ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
have neg : ∀ (h : ∃ y ∈ s, f y < f x), ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Tactic: by_cases! h : ∀ y ∈ s, f x ≤ f y
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
Goal:
α : 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
have neg : ∀ (w : α) (hw : w ∈ s) (hwx : f w < f x), ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Tactic: obtain ⟨w, hw, hwx⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
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
have neg : ∀ (y : α) (hy : y ∈ s), (f w).succ ≤ (f y).succ
Tactic: refine ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ ?_, hs hy hw⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Equitable (goal)
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 w).succ ≤ (f y).succ
have neg : f x ≤ (f y).succ
Tactic: rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]