awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ ¬Disjoint s t ↔ ∃ (x : α), x ∈ s ∧ x ∈ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ ¬Disjoint s t ↔ (s ∩ t).Nonempty

Tactic:
not_disjoint_iff

Premises used: Set.Mem, setOf, Set.inter, Set.not_disjoint_iff, Set.Nonempty
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ Disjoint s t ∨ (s ∩ t).Nonempty

Tactic:
(em _).imp_right not_disjoint_iff_nonempty_inter.1

Premises used: em, Set.not_disjoint_iff_nonempty_inter, Iff.mp, Or.imp_right
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b

Tactic:
grind
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t u : Set α
h : s ⊆ u
d : Disjoint u t
⊢ Disjoint s t

Tactic:
d.mono_left h

Premises used: Disjoint.mono_left
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t u : Set α
h : t ⊆ u
d : Disjoint s u
⊢ Disjoint s t

Tactic:
d.mono_right h

Premises used: Disjoint.mono_right
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
h : Disjoint s₂ t₂
⊢ Disjoint s₁ t₁

Tactic:
h.mono hs ht

Premises used: Disjoint.mono
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t u : Set α
⊢ Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
disjoint_sup_left

Premises used: disjoint_sup_left
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t u : Set α
⊢ Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
disjoint_sup_right

Premises used: disjoint_sup_right
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s : Set α
⊢ Disjoint s ∅

Tactic:
disjoint_bot_right

Premises used: disjoint_bot_right
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s : Set α
⊢ Disjoint ∅ s

Tactic:
disjoint_bot_left

Premises used: disjoint_bot_left
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s : Set α
⊢ Disjoint univ s ↔ s = ∅

Tactic:
top_disjoint

Premises used: top_disjoint
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s : Set α
⊢ Disjoint s univ ↔ s = ∅

Tactic:
disjoint_top

Premises used: disjoint_top
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
β : Sort u_1
γ : Sort u_2
x : β → α
y : γ → α
⊢ Disjoint (range x) (range y) ↔ ∀ (i : β) (j : γ), x i ≠ y j

Tactic:
simp [Set.disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
hs : Disjoint s u
ht : Disjoint t u
⊢ Disjoint (s ∪ t) u

Tactic:
hs.sup_left ht

Premises used: Disjoint.sup_left
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
ht : Disjoint s t
hu : Disjoint s u
⊢ Disjoint s (t ∪ u)

Tactic:
ht.sup_right hu

Premises used: Disjoint.sup_right
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
h : Disjoint s t
⊢ Disjoint (s ∩ u) t

Tactic:
h.inf_left _

Premises used: Disjoint.inf_left
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
h : Disjoint s t
⊢ Disjoint (u ∩ s) t

Tactic:
h.inf_left' _

Premises used: Disjoint.inf_left'
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
h : Disjoint s t
⊢ Disjoint s (t ∩ u)

Tactic:
h.inf_right _

Premises used: Disjoint.inf_right
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
h : Disjoint s t
⊢ Disjoint s (u ∩ t)

Tactic:
h.inf_right' _

Premises used: Disjoint.inf_right'
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
h : s ⊆ t ∪ u
hac : Disjoint s u
⊢ s ⊆ t

Tactic:
hac.left_le_of_le_sup_right h

Premises used: Disjoint.left_le_of_le_sup_right
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t u : Set α
h : s ⊆ t ∪ u
hab : Disjoint s t
⊢ s ⊆ u

Tactic:
hab.left_le_of_le_sup_left h

Premises used: Disjoint.left_le_of_le_sup_left
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)

Tactic:
grind [Xor]

Premises used: Xor
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
⊢ dissipate s x = ⋂ (y : α), ⋂ (_ : y ≤ x), s y

Tactic:
rfl

Premises used: Set.dissipate, rfl
-- Module: Mathlib.Data.Set.Dissipate
Goal:
β : Type u_2
s : ℕ → Set β
n : ℕ
simp_rw : dissipate s n = ⋂ (k : ℕ), ⋂ (_ : k ≤ n), s k
⊢ dissipate s n = ⋂ (k : ℕ), ⋂ (_ : k < n + 1), s k

Tactic:
simp_rw [Nat.lt_add_one_iff, dissipate]

Premises used: Set.dissipate, Nat.lt_add_one_iff
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
z : β
⊢ z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y

Tactic:
simp [dissipate_def]

Premises used: Set.dissipate_def
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x y : α
hy : y ≤ x
⊢ dissipate s x ⊆ s y

Tactic:
biInter_subset_of_mem hy

Premises used: Set.dissipate, Set.Mem, Set.biInter_subset_of_mem
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
simp : ∀ (i : α) (i_1 : i ≤ x), ⋂ (i : α), s i ⊆ s i
⊢ ⋂ (i : α), s i ⊆ dissipate s x

Tactic:
simp only [dissipate, subset_iInter_iff]

Premises used: Set.dissipate, Set.subset_iInter_iff
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
⊢ ∀ (i : α) (i_1 : i ≤ x), ⋂ (i : α), s i ⊆ s i

Tactic:
fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a

Premises used: Set.iInter_subset_of_subset
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
⊢ ∀ (i : α) (i_1 : i ≤ x), ⋂ (i : α), s i ⊆ s i

Tactic:
exact fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a

Premises used: Set.iInter_subset_of_subset
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Antitone (dissipate s)

Tactic:
fun _ _ hab ↦ biInter_subset_biInter_left fun _ hz => le_trans hz hab

Premises used: Set.dissipate, Set.Mem, Set.biInter_subset_biInter_left, Antitone, le_trans
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x y : α
h : y ≤ x
⊢ dissipate s x ⊆ dissipate s y

Tactic:
antitone_dissipate h

Premises used: Set.antitone_dissipate
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
h₁ : ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x
h₂ : dissipate s x ⊆ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y
⊢ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y = dissipate s x

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
apply :
  ∀ (z : α) (y : β) (hy : Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), dissipate s z) y),
    Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), s z) y
⊢ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x

Tactic:
apply iInter_mono fun z y hy ↦ ?_

Premises used: Set.iInter_mono
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x z : α
y : β
hy : Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), dissipate s z) y
simp : ∀ (hy : ∀ (i : z ≤ x), ∀ y_1 ≤ z, y ∈ s y_1) (i : z ≤ x), y ∈ s z
⊢ Membership.mem (γ := Set β) (⋂ (_ : z ≤ x), s z) y

Tactic:
simp only [mem_iInter, mem_dissipate] at *

Premises used: Set.mem_dissipate, Set.mem_iInter
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x z : α
y : β
hy : ∀ (i : z ≤ x), ∀ y_1 ≤ z, y ∈ s y_1
⊢ ∀ (i : z ≤ x), y ∈ s z

Tactic:
fun h ↦ hy h z le_rfl

Premises used: le_rfl
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x z : α
y : β
hy : ∀ (i : z ≤ x), ∀ y_1 ≤ z, y ∈ s y_1
⊢ ∀ (i : z ≤ x), y ∈ s z

Tactic:
exact fun h ↦ hy h z le_rfl

Premises used: le_rfl
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
h₂ : ∀ (i : α) (i_1 : i ≤ x), dissipate s x ⊆ dissipate s i
⊢ dissipate s x ⊆ ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y

Tactic:
simp only [subset_iInter_iff]

Premises used: Set.subset_iInter_iff
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
⊢ ∀ (i : α) (i_1 : i ≤ x), dissipate s x ⊆ dissipate s i

Tactic:
fun i j ↦ dissipate_subset_dissipate j

Premises used: Set.dissipate_subset_dissipate
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
x : α
⊢ ∀ (i : α) (i_1 : i ≤ x), dissipate s x ⊆ dissipate s i

Tactic:
exact fun i j ↦ dissipate_subset_dissipate j

Premises used: Set.dissipate_subset_dissipate
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
h₁ : Subset.{u_2} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)
h₂ : Subset.{u_2} (α := Set β) (⋂ (x : α), s x) (⋂ (x : α), dissipate s x)
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
h₁ : ∀ (x : β), (∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1) → ∀ (i : α), x ∈ s i
⊢ Subset.{u_2} (α := Set β) (⋂ (x : α), dissipate s x) (⋂ (x : α), s x)

Tactic:
simp_rw [subset_def, dissipate_def, mem_iInter]

Premises used: Set.subset_def, Set.dissipate_def, Set.mem_iInter
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
h₂ : ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1
⊢ Subset.{u_2} (α := Set β) (⋂ (x : α), s x) (⋂ (x : α), dissipate s x)

Tactic:
simp_rw [subset_def, dissipate_def, mem_iInter]

Premises used: Set.subset_def, Set.dissipate_def, Set.mem_iInter
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ ∀ (x : β), (∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1) → ∀ (i : α), x ∈ s i

Tactic:
fun z h x' ↦ h x' x' le_rfl

Premises used: le_rfl
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ ∀ (x : β), (∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1) → ∀ (i : α), x ∈ s i

Tactic:
exact fun z h x' ↦ h x' x' le_rfl
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1

Tactic:
fun z h x' y hy ↦ h y
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α) (i : i_1 ≤ i), x ∈ s i_1

Tactic:
exact fun z h x' y hy ↦ h y
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
s : α → Set β
⊢ dissipate s ⊥ = s ⊥

Tactic:
simp [dissipate_def]

Premises used: Set.dissipate_def
-- Module: Mathlib.Data.Set.Dissipate
Goal:
β : Type u_2
s : ℕ → Set β
⊢ dissipate s 0 = s 0

Tactic:
simp [dissipate_def]

Premises used: Set.dissipate_def
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
n : ℕ
h : ∀ (x : α), x ∈ dissipate s (n + 1) ↔ x ∈ dissipate s n ∩ s (n + 1)
⊢ dissipate s (n + 1) = dissipate s n ∩ s (n + 1)

Tactic:
ext x
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
n : ℕ
x : α
h : (∀ (i : ℕ) (i_1 : i ≤ n + 1), x ∈ s i) ↔ (∀ (i : ℕ) (i_1 : i ≤ n), x ∈ s i) ∧ x ∈ s (n + 1)
⊢ x ∈ dissipate s (n + 1) ↔ x ∈ dissipate s n ∩ s (n + 1)

Tactic:
simp_all only [dissipate_def, mem_iInter, mem_inter_iff]

Premises used: Set.dissipate_def, Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
n : ℕ
x : α
⊢ (∀ (i : ℕ) (i_1 : i ≤ n + 1), x ∈ s i) ↔ (∀ (i : ℕ) (i_1 : i ≤ n), x ∈ s i) ∧ x ∈ s (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
h : s 0 ⊆ dissipate s 0
⊢ ∃ (m : ℕ), s m ⊆ dissipate s 0

Tactic:
use 0
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
⊢ s 0 ⊆ dissipate s 0

Tactic:
simp [dissipate_def]

Premises used: Set.dissipate_def
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n : ℕ
hn : ∃ (m : ℕ), s m ⊆ dissipate s n
succ : ∀ (m : ℕ) (hm : s m ⊆ dissipate s n), ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)
⊢ ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)

Tactic:
obtain ⟨m, hm⟩ := hn
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n m : ℕ
hm : s m ⊆ dissipate s n
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)
⊢ ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)

Tactic:
obtain ⟨k, hk⟩ := hd m (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Set.Dissipate
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)
simp : s k ⊆ dissipate s n ∧ s k ⊆ s (n + 1)
⊢ s k ⊆ dissipate s (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Set.Dissipate
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 ∧ s k ⊆ s (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Set.Dissipate
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)
⊢ ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)

Tactic:
exact ⟨k, by simp; grind⟩
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
n : ℕ
zero : ∃ (m : ℕ), s m ⊆ dissipate s 0
succ : ∀ (n : ℕ) (hn : ∃ (m : ℕ), s m ⊆ dissipate s n), ∃ (m : ℕ), s m ⊆ dissipate s (n + 1)
⊢ ∃ (m : ℕ), s m ⊆ dissipate s n

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⟩

Premises used: Set.dissipate_def
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) (dissipate s)

Tactic:
antitone_dissipate.directed_ge

Premises used: Antitone.directed_ge, Set.antitone_dissipate
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
⊢ (∃ (n : ℕ), dissipate s n = ∅) ↔ ∃ (n : ℕ), s n = ∅

Tactic:
⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩⟩

Premises used: Set.dissipate, le_rfl, Exists, _private.0.Set.exists_dissipate_eq_empty_iff_of_directed.match_1, Iff.intro, Exists.intro, Set.dissipate_subset, EmptyCollection.emptyCollection, Eq, Set.subset_eq_empty
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
refine : (∃ (n : ℕ), dissipate s n = ∅) → ∃ (n : ℕ), s n = ∅
⊢ (∃ (n : ℕ), dissipate s n = ∅) ↔ ∃ (n : ℕ), s n = ∅

Tactic:
refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩⟩
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
contrapose! : (∀ (n : ℕ), (s n).Nonempty) → ∀ (n : ℕ), (dissipate s n).Nonempty
⊢ (∃ (n : ℕ), dissipate s n = ∅) → ∃ (n : ℕ), s n = ∅

Tactic:
contrapose!
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
h : ∀ (n : ℕ), (s n).Nonempty
n : ℕ
obtain : ∀ (m : ℕ) (hm : s m ⊆ dissipate s n), (dissipate s n).Nonempty
⊢ (dissipate s n).Nonempty

Tactic:
obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n

Premises used: Set.exists_subset_dissipate_of_directed
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
h : ∀ (n : ℕ), (s n).Nonempty
n m : ℕ
hm : s m ⊆ dissipate s n
⊢ (dissipate s n).Nonempty

Tactic:
(h m).mono hm

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Data.Set.Dissipate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) s
h : ∀ (n : ℕ), (s n).Nonempty
n m : ℕ
hm : s m ⊆ dissipate s n
⊢ (dissipate s n).Nonempty

Tactic:
exact (h m).mono hm

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
⊢ enumerate sel s 0 = none

Tactic:
simp [h, enumerate]

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ enumerate sel s (n + 1) = none

Tactic:
simp [h, enumerate]

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
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
some : ∀ (val : α) (hs : sel s = Option.some val), enumerate sel s m = Option.none
⊢ enumerate sel s m = Option.none

Tactic:
cases hs : sel s
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
hs : sel s = none
⊢ enumerate sel s m = none

Tactic:
enumerate_eq_none_of_sel sel hs

Premises used: Set.enumerate_eq_none_of_sel
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
hs : sel s = none
⊢ enumerate sel s m = none

Tactic:
exact enumerate_eq_none_of_sel sel hs

Premises used: Set.enumerate_eq_none_of_sel
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val : α
hs : sel s = some val
hm : n + 1 ≤ 0
⊢ enumerate sel s 0 = none

Tactic:
contradiction
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val : α
hs : sel s = Option.some val
m' : ℕ
hm : n + 1 ≤ m' + 1
some :
  ∀
    (h :
      Eq (α := Option α)
        (do
          let a ← Option.some val
          enumerate sel (s \ {a}) n)
        none),
    Eq (α := Option α)
      (do
        let a ← Option.some val
        enumerate sel (s \ {a}) m')
      none
⊢ enumerate sel s (m' + 1) = none

Tactic:
simp only [enumerate, hs] at h ⊢

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
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
⊢ n ≤ m'

Tactic:
have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val : α
hs : sel s = some val
m' : ℕ
hm_1 : n + 1 ≤ m' + 1
h :
  Eq (α := Option α)
    (do
      let a ← some val
      enumerate sel (s \ {a}) n)
    none
hm : n ≤ m'
⊢ Eq (α := Option α)
    (do
      let a ← some val
      enumerate sel (s \ {a}) m')
    none

Tactic:
enumerate_eq_none h hm
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val : α
hs : sel s = some val
m' : ℕ
hm_1 : n + 1 ≤ m' + 1
h :
  Eq (α := Option α)
    (do
      let a ← some val
      enumerate sel (s \ {a}) n)
    none
hm : n ≤ m'
⊢ Eq (α := Option α)
    (do
      let a ← some val
      enumerate sel (s \ {a}) m')
    none

Tactic:
exact enumerate_eq_none h hm
-- Module: Mathlib.Data.Set.Enumerate
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
some₁ : ∀ (m' : ℕ) (hm : n + 1 ≤ m' + 1), enumerate sel s (m' + 1) = none
⊢ enumerate sel s m = 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

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
simp [enumerate_eq_none_of_sel, h]

Premises used: Set.enumerate_eq_none_of_sel
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = Option.some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = Option.some a'
some :
  (do
        let a ← Option.some a'
        enumerate sel (s \ {a}) n) =
      Option.some a →
    a ∈ s
⊢ enumerate sel s (n + 1) = Option.some a → a ∈ s

Tactic:
simp only [enumerate, h]

Premises used: Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
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'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s

Tactic:
fun h' : enumerate sel (s \ {a'}) n = some a ↦
        have : a ∈ s \ {a'} := enumerate_mem h_sel h'
        this.left

Premises used: And.left
-- Module: Mathlib.Data.Set.Enumerate
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'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s

Tactic:
exact fun h' : enumerate sel (s \ {a'}) n = some a ↦
        have : a ∈ s \ {a'} := enumerate_mem h_sel h'
        this.left

Premises used: And.left
-- Module: Mathlib.Data.Set.Enumerate
Goal:
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
cases : ∀ (x : Option α) (h : sel s = x), enumerate sel s (n + 1) = some a → a ∈ s
⊢ 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

Premises used: Option.some, Set.enumerate_eq_none_of_sel, Option.none, Set.enumerate
-- Module: Mathlib.Data.Set.Enumerate
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₂
wlog! : ∀ {n₁ n₂ : ℕ} (h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) (hn : n₁ ≤ n₂), n₁ = n₂
⊢ n₁ = n₂

Tactic:
wlog! hn : n₁ ≤ n₂ generalizing n₁ n₂
-- Module: Mathlib.Data.Set.Enumerate
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
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:
(this h₂ h₁ hn.le).symm

Premises used: LT.lt.le, Eq.symm
-- Module: Mathlib.Data.Set.Enumerate
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
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:
exact (this h₂ h₁ hn.le).symm

Premises used: LT.lt.le, Eq.symm