awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
rw rw₁ rw₂ :
  ∀ (hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x)
    {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i), ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
rw₃ :
  ∀ (hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x)
    {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i), ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
rw₄ :
  ∀ (hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x)
    {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i),
    let g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i;
    ∀ (h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)), ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
rw₅ :
  ∀ (hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x)
    {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i),
    let g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i;
    ∀ (h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)) (h2 : k ≤ sSup (range g)),
      ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
rw₆ :
  ∀ (hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x)
    {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i),
    let g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i;
    ∀ (h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)) (h2 : k ≤ sSup (range g)) (s : Finset ι) (hs : k ≤ g s),
      ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i

Tactic:
classical
    rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
    let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
    have h1 : DirectedOn (· ≤ ·) (Set.range g) := by
      rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
      exact
        ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
          iSup_le_iSup_of_subset Finset.subset_union_right⟩
    have h2 : k ≤ sSup (Set.range g) :=
      h.trans
        (iSup_le fun i =>
          le_sSup_of_le ⟨{i}, rfl⟩
            (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
    obtain ⟨-, ⟨s, rfl⟩, hs⟩ := hk (Set.range g) (Set.range_nonempty g) h1 h2
    exact ⟨s, hs⟩

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
rw :
  ∀ (hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x)
    {s : Set α} (hemp : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s) (hbelow : ∀ x ∈ s, x < k),
    sSup s < k
⊢ sSup s < k

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
by_contra : ∀ (h : ¬sSup s < k), False
⊢ sSup s < k

Tactic:
by_contra h
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬sSup s < k
⊢ sSup s ≤ k

Tactic:
have sSup' : sSup s ≤ k := sSup_le fun s hs => (hbelow s hs).le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬sSup s < k
sSup' : sSup s ≤ k
⊢ sSup s = k

Tactic:
replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
obtain : ∀ (x : α) (hxs : x ∈ s) (hkx : k ≤ x), False
⊢ False

Tactic:
obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le

Premises used: Eq.le, Eq.symm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
⊢ x < k

Tactic:
obtain hxk := hbelow x hxs
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
hxk : x < k
⊢ False

Tactic:
hxk.ne (hxk.le.antisymm hkx)

Premises used: LE.le.antisymm, LT.lt.le, LT.lt.ne
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
hxk : x < k
⊢ False

Tactic:
exact hxk.ne (hxk.le.antisymm hkx)

Premises used: LE.le.antisymm, LT.lt.le, LT.lt.ne
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
simp_rw :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (s_1 : Set α),
    s_1.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s_1 → s.sup f ≤ sSup s_1 → ∃ x ∈ s_1, s.sup f ≤ x
⊢ IsCompactElement (s.sup f)

Tactic:
simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
rw : ∃ x ∈ d, s.sup (id ∘ f) ≤ x
⊢ ∃ x ∈ d, s.sup f ≤ x

Tactic:
rw [← Function.id_comp f]

Premises used: Function.id_comp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
rw : ∃ x ∈ d, (Finset.image f s).sup id ≤ x
⊢ ∃ x ∈ d, s.sup (id ∘ f) ≤ x

Tactic:
rw [← Finset.sup_image]

Premises used: Finset.sup_image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
a : ∀ x ∈ Finset.image f s, ∃ y ∈ d, x ≤ y
⊢ ∃ x ∈ d, (Finset.image f s).sup id ≤ x

Tactic:
apply Finset.sup_le_of_le_directed d hemp hdir

Premises used: Finset.sup_le_of_le_directed
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
x : α
hx : x ∈ Finset.image f s
a : ∀ (p : β) (hps : p ∈ s) (hx : f p ∈ Finset.image f s), ∃ y ∈ d, f p ≤ y
⊢ ∃ y ∈ d, x ≤ y

Tactic:
obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
⊢ ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f p ≤ sSup s → ∃ x ∈ s, f p ≤ x

Tactic:
specialize h p hps
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f p ≤ sSup s → ∃ x ∈ s, f p ≤ x
⊢ ∃ x ∈ d, f p ≤ x

Tactic:
specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)

Premises used: Finset.le_sup, le_trans
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∃ x ∈ d, f p ≤ x
⊢ ∃ y ∈ d, f p ≤ y

Tactic:
simpa only [exists_prop]

Premises used: exists_prop
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
simp_rw simp_rw₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup f ≤ x
simp_rw₂ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup (id ∘ f) ≤ x
simp_rw₃ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, (Finset.image f s).sup id ≤ x
a a₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (x : α)
    (hx : x ∈ Finset.image f s), ∃ y ∈ d, x ≤ y
a₂ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
    (hps : p ∈ s) (hx : f p ∈ Finset.image f s), ∃ y ∈ d, f p ≤ y
a₃ :
  ∀ (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
    (hps : p ∈ s) (hx : f p ∈ Finset.image f s)
    (h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f p ≤ sSup s → ∃ x ∈ s, f p ≤ x),
    ∃ y ∈ d, f p ≤ y
a₄ :
  ∀ (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
    (hps : p ∈ s) (hx : f p ∈ Finset.image f s) (h : ∃ x ∈ d, f p ≤ x), ∃ y ∈ d, f p ≤ y
⊢ IsCompactElement (s.sup f)

Tactic:
classical
    simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h
    intro d hemp hdir hsup
    rw [← Function.id_comp f]
    rw [← Finset.sup_image]
    apply Finset.sup_le_of_le_directed d hemp hdir
    rintro x hx
    obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
    specialize h p hps
    specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
    simpa only [exists_prop]

Premises used: exists_prop, Finset.sup_image, CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le, rfl, Function.id_comp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
⊢ (↑∅ : Set α) ⊆ s ∧ Eq.{u_2 + 1} (α := α) (Finset.sup ∅ id) ⊥

Tactic:
simp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
obtain :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (hm : ∀ x ∈ S, ¬t.sup id < x),
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id

Tactic:
obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩

Premises used: Bot.bot, Exists.intro, wellFounded_gt, WellFounded.has_min, EmptyCollection.emptyCollection, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id

Tactic:
⟨t, ht₁, (sSup_le fun y hy => ?_).antisymm ?_⟩

Premises used: LE.le.antisymm, And.intro, Exists.intro, sSup_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
refine_1 : ∀ (y : α) (hy : y ∈ s), y ≤ t.sup id
refine_2 : t.sup id ≤ sSup s
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id

Tactic:
refine ⟨t, ht₁, (sSup_le fun y hy => ?_).antisymm ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ (↑(insert y t) : Set α) ⊆ s ∧ (insert y t).sup id = (insert y t).sup id

Tactic:
simp [Set.insert_subset_iff, hy, ht₁]

Premises used: Set.insert_subset_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
refine_1 : y ≤ (insert y t).sup id
⊢ y ≤ t.sup id

Tactic:
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]

Premises used: Insert.insert, Finset.sup_mono, Exists.intro, Finset.subset_insert, eq_of_le_of_not_lt
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ (insert y t).sup id

Tactic:
simp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
refine_1 refine_1₁ refine_1₂ : y ≤ (insert y t).sup id
⊢ y ≤ t.sup id

Tactic:
classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
refine_2 : sSup (↑t : Set α) ≤ sSup s
⊢ t.sup id ≤ sSup s

Tactic:
rw [Finset.sup_id_eq_sSup]

Premises used: Finset.sup_id_eq_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ sSup (↑t : Set α) ≤ sSup s

Tactic:
sSup_le_sSup ht₁

Premises used: sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ sSup (↑t : Set α) ≤ sSup s

Tactic:
exact sSup_le_sSup ht₁

Premises used: sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
obtain : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := h s
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
inl : ∀ (ht₁ : (↑∅ : Set α) ⊆ s) (ht₂ : sSup s = Finset.sup ∅ id), sSup s ∈ s
inr : ∀ (h : t.Nonempty), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
rcases t.eq_empty_or_nonempty with rfl | h

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : (↑∅ : Set α) ⊆ s
ht₂ : sSup s = Finset.sup ∅ id
⊢ sSup s = ⊥

Tactic:
rw [Finset.sup_empty] at ht₂

Premises used: Finset.sup_empty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : (↑∅ : Set α) ⊆ s
ht₂ : sSup s = ⊥
inl : ⊥ ∈ s
⊢ sSup s ∈ s

Tactic:
rw [ht₂]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : (↑∅ : Set α) ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s

Tactic:
simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]

Premises used: eq_singleton_bot_of_sSup_eq_bot_of_nonempty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
inr : t.sup id ∈ s
⊢ sSup s ∈ s

Tactic:
rw [ht₂]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ t.sup id ∈ s

Tactic:
hsc.finsetSup_mem h ht₁

Premises used: SupClosed.finsetSup_mem
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ t.sup id ∈ s

Tactic:
exact hsc.finsetSup_mem h ht₁

Premises used: SupClosed.finsetSup_mem
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
⊢ WellFounded fun (x1 x2 : α) ↦ x2 < x1

Tactic:
RelEmbedding.wellFounded_iff_isEmpty.mpr ⟨fun a => ?_⟩

Premises used: Iff.mpr, IsEmpty.mk, RelEmbedding.wellFounded_iff_isEmpty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
refine : ∀ (a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1), False
⊢ WellFounded fun (x1 x2 : α) ↦ x2 < x1

Tactic:
refine RelEmbedding.wellFounded_iff_isEmpty.mpr ⟨fun a => ?_⟩

Premises used: Iff.mpr, IsEmpty.mk, RelEmbedding.wellFounded_iff_isEmpty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
obtain : ∀ (n : ℕ) (hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)), False
⊢ False

Tactic:
obtain ⟨n, hn⟩ := Set.mem_range.mp this

Premises used: Set.mem_range, Iff.mp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
n : ℕ
hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
change : GT.gt (α := α) ((a : (a : ℕ) → α) (n + 1) : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
⊢ LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)

Tactic:
change _ > _
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
n : ℕ
hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
⊢ GT.gt (α := α) ((a : (a : ℕ) → α) (n + 1) : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)

Tactic:
simp [← hn, a.map_rel_iff]

Premises used: RelEmbedding.map_rel_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
n : ℕ
hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
⊢ LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)

Tactic:
have h' : sSup (Set.range a) < a (n + 1) := by
        change _ > _
        simp [← hn, a.map_rel_iff]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
n : ℕ
hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
h' : LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)
apply : LT.lt (α := α) ((a : (a : ℕ) → α) (n + 1) : α) ((a : (a : ℕ) → α) (n + 1) : α)
⊢ False

Tactic:
apply lt_irrefl (a (n + 1))

Premises used: lt_irrefl, HAdd.hAdd, OfNat.ofNat, DFunLike.coe