awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u
inst : CompleteLattice α
k : α
rw rw₁ rw₂ :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) ↔
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
have mp : (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) →
  ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
Tactic: classical
    rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
    constructor
    · intro H ι s hs
      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
      choose f hf using this
      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
      rw [Finset.sup_le_iff]
      intro b hb
      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
    · intro H s hs
      obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])
      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
      rw [Finset.sup_le_iff]
      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u
inst : CompleteLattice α
k : α
rw rw₁ rw₂ :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) ↔
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
mp :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) →
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
have mpr : (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s) →
  ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: classical
    rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
    constructor
    · intro H ι s hs
      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
      choose f hf using this
      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
      rw [Finset.sup_le_iff]
      intro b hb
      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
    · intro H s hs
      obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])
      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
      rw [Finset.sup_le_iff]
      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
have 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
Tactic: rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
Cleared hypotheses: hk, ι, f, h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
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
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
have h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)
Tactic: 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⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
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
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
have h2 : k ≤ sSup (range g)
Tactic: 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)))
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
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
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
have obtain : ∀ (s : Finset ι) (hs : k ≤ g s), ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
Tactic: obtain ⟨-, ⟨s, rfl⟩, hs⟩ := hk (Set.range g) (Set.range_nonempty g) h1 h2
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
have 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
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⟩
Cleared hypotheses: hk, ι, f, h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
have 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
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⟩
Cleared hypotheses: hk, ι, f, h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
have 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
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⟩
Cleared hypotheses: hk, ι, f, h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
have 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
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⟩
Cleared hypotheses: hk, ι, f, h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ sSup s < k
have 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
Tactic: rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
Cleared hypotheses: hk, s, hemp, hdir, hbelow
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ sSup s < k
have by_contra : ∀ (h : ¬sSup s < k), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ False
have sSup' : sSup s ≤ k
Tactic: have sSup' : sSup s ≤ k := sSup_le fun s hs => (hbelow s hs).le
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ False
have sSup : sSup s = k
Tactic: replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ False
have obtain : ∀ (x : α) (hxs : x ∈ s) (hkx : k ≤ x), False
Tactic: obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ False
have hxk : x < k
Tactic: obtain hxk := hbelow x hxs
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ IsCompactElement (s.sup f)
have 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
Tactic: simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ∈ d, s.sup f ≤ x
have rw : ∃ x ∈ d, s.sup (id ∘ f) ≤ x
Tactic: rw [← Function.id_comp f]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ∈ d, s.sup (id ∘ f) ≤ x
have rw : ∃ x ∈ d, (Finset.image f s).sup id ≤ x
Tactic: rw [← Finset.sup_image]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ∈ d, (Finset.image f s).sup id ≤ x
have a : ∀ x ∈ Finset.image f s, ∃ y ∈ d, x ≤ y
Tactic: apply Finset.sup_le_of_le_directed d hemp hdir
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ y ∈ d, x ≤ y
have a : ∀ (p : β) (hps : p ∈ s) (hx : f p ∈ Finset.image f s), ∃ y ∈ d, f p ≤ y
Tactic: obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ ∃ y ∈ d, f p ≤ y
have h₁ : ∀ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ IsCompactElement (s.sup f)
have 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
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ IsCompactElement (s.sup f)
have 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
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ IsCompactElement (s.sup f)
have 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
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ IsCompactElement (s.sup f)
have 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 ∈ Finset.image f s, ∃ y ∈ d, x ≤ y
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]
Cleared hypotheses: h