awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
rw : x ≤ sSup s
⊢ x = ⊥

Tactic:
rw [← hs, eq_comm, inf_eq_left]

Premises used: eq_comm, inf_eq_left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s

Tactic:
le_sSup hx₀

Premises used: le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s

Tactic:
exact le_sSup hx₀

Premises used: le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (contra : s.Infinite), False
by_contra!₁₁ : ∀ (contra : s.Infinite) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
by_contra!₁₂ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t), False
by_contra!₁₃ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t),
    False
by_contra!₁₄ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
    (hs : x ⊓ sSup s = ⊥), False
by_contra!₁₅ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
    (hs : x ⊓ sSup s = ⊥), x = ⊥
by_contra!₁₆ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
    (hs : x ⊓ sSup s = ⊥), x ≤ sSup s
⊢ s.Finite

Tactic:
classical
    by_contra! contra
    obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s
    replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t := by
      have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
      obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
      exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
    obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
    replace hs : x ⊓ sSup s = ⊥ := by
      have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
      simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
    apply hx₁
    rw [← hs, eq_comm, inf_eq_left]
    exact le_sSup hx₀

Premises used: CompleteLattice.WellFoundedGT.isSupFiniteCompact, eq_comm, inf_eq_left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ Set.Finite.{u_3} (α := ι) {i : ι | t i ≠ ⊥}

Tactic:
Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Premises used: Set.image_subset_range, Set.Finite.subset, iSupIndep.injOn, Set.Finite.of_finite_image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
refine : (range t).Finite
⊢ Set.Finite.{u_3} (α := ι) {i : ι | t i ≠ ⊥}

Tactic:
refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Premises used: Set.image_subset_range, Set.Finite.subset, iSupIndep.injOn, Set.Finite.of_finite_image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Tactic:
WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range

Premises used: WellFoundedGT.finite_of_sSupIndep, iSupIndep.sSupIndep_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Tactic:
exact WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range

Premises used: WellFoundedGT.finite_of_sSupIndep, iSupIndep.sSupIndep_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Finite ι

Tactic:
haveI := (WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range).to_subtype
  Finite.of_injective_finite_range (ht.injective h_ne_bot)

Premises used: iSupIndep.injective, Finite.of_injective_finite_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
by_contra : ∀ (inf : ¬s.Finite), False
⊢ s.Finite

Tactic:
by_contra inf
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
⊢ ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n

Tactic:
have sup_le n : (e n).1 ⊔ a (n + 1) ≤ a n := sup_le_iff.mpr ⟨le_iSup₂_of_le n le_rfl le_rfl,
    iSup₂_le fun i hi ↦ le_iSup₂_of_le i (n.le_succ.trans hi) le_rfl⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
refine_2 : ∀ (lt : ∀ (n : ℕ), a (n + 1) < a n), False
refine_1 :
  ∀ (n i : ℕ) (hi : i ≥ n + 1),
    (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α) ∈ s \ {(↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α)}
⊢ False

Tactic:
have lt n : a (n + 1) < a n := (Disjoint.right_lt_sup_of_left_ne_bot
    ((hs (e n).2.1).mono_right <| iSup₂_le fun i hi ↦ le_sSup ?_) (e n).2.2).trans_le (sup_le n)
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
lt : ∀ (n : ℕ), a (n + 1) < a n
⊢ False

Tactic:
(RelEmbedding.natGT a lt).not_wellFounded wellFounded_lt

Premises used: RelEmbedding.natGT, RelEmbedding.not_wellFounded, wellFounded_lt
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
lt : ∀ (n : ℕ), a (n + 1) < a n
⊢ False

Tactic:
exact (RelEmbedding.natGT a lt).not_wellFounded wellFounded_lt

Premises used: RelEmbedding.natGT, RelEmbedding.not_wellFounded, wellFounded_lt
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
n i : ℕ
hi : i ≥ n + 1
⊢ (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α) ∈ s \ {(↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α)}

Tactic:
⟨(e i).2.1, fun h ↦ n.lt_succ_self.not_ge <| hi.trans_eq <| e.2 <| Subtype.val_injective h⟩

Premises used: LE.le.trans_eq, Set.Mem, Subtype.val_injective, Set.diff, setOf, Nat.lt_succ_self, Function.Embedding.inj', And.left, And.intro, LT.lt.not_ge, DFunLike.coe, Subtype.property
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
n i : ℕ
hi : i ≥ n + 1
⊢ (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α) ∈ s \ {(↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α)}

Tactic:
exact ⟨(e i).2.1, fun h ↦ n.lt_succ_self.not_ge <| hi.trans_eq <| e.2 <| Subtype.val_injective h⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ Set.Finite.{u_3} (α := ι) {i : ι | t i ≠ ⊥}

Tactic:
Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Premises used: Set.image_subset_range, Set.Finite.subset, iSupIndep.injOn, Set.Finite.of_finite_image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
refine : (range t).Finite
⊢ Set.Finite.{u_3} (α := ι) {i : ι | t i ≠ ⊥}

Tactic:
refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Premises used: Set.image_subset_range, Set.Finite.subset, iSupIndep.injOn, Set.Finite.of_finite_image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Tactic:
WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range

Premises used: WellFoundedLT.finite_of_sSupIndep, iSupIndep.sSupIndep_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Tactic:
exact WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range

Premises used: WellFoundedLT.finite_of_sSupIndep, iSupIndep.sSupIndep_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Finite ι

Tactic:
haveI := (WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range).to_subtype
  Finite.of_injective_finite_range (ht.injective h_ne_bot)

Premises used: iSupIndep.injective, Finite.of_injective_finite_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
b : α
rcases : ∀ (s : Set α) (hs : ∀ x ∈ s, IsCompactElement x), sSup {c : α | IsCompactElement c ∧ c ≤ sSup s} = sSup s
⊢ sSup {c : α | IsCompactElement c ∧ c ≤ b} = b

Tactic:
rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩

Premises used: IsCompactlyGenerated.exists_sSup_eq, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
⊢ sSup {c : α | IsCompactElement c ∧ c ≤ sSup s} = sSup s

Tactic:
le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)

Premises used: le_antisymm, And.right, And.intro, le_sSup, sSup_le, sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
⊢ sSup {c : α | IsCompactElement c ∧ c ≤ sSup s} = sSup s

Tactic:
exact le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
rw : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) (sSup {c : α | IsCompactElement c ∧ c ≤ ⊤})
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) ⊤

Tactic:
rw [← sSup_compact_le_eq ⊤]

Premises used: sSup_compact_le_eq, Top.top
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
simp_rw : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) (sSup {c : α | IsCompactElement c ∧ True})
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) (sSup {c : α | IsCompactElement c ∧ c ≤ ⊤})

Tactic:
simp_rw [le_top, and_true]

Premises used: and_true, le_top
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
rw : LE.le.{u_2} (α := α) (sSup {c : α | IsCompactElement c ∧ c ≤ a}) (sSup {c : α | IsCompactElement c ∧ c ≤ b})
⊢ a ≤ b

Tactic:
rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]

Premises used: sSup_compact_le_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
⊢ LE.le.{u_2} (α := α) (sSup {c : α | IsCompactElement c ∧ c ≤ a}) (sSup {c : α | IsCompactElement c ∧ c ≤ b})

Tactic:
sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩

Premises used: And.right, And.left, And.intro, sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
⊢ LE.le.{u_2} (α := α) (sSup {c : α | IsCompactElement c ∧ c ≤ a}) (sSup {c : α | IsCompactElement c ∧ c ≤ b})

Tactic:
exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
rw : ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [le_iff_compact_le_imp]

Premises used: le_iff_compact_le_imp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
pos : ∀ (hs : s.Nonempty) (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
neg : ∀ (hs : ¬s.Nonempty) (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
by_cases hs : s.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
hc₁ : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
⊢ c ≤ a ⊓ sSup s

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ a ∧ c ≤ sSup s

Tactic:
rw [le_inf_iff] at hcinf

Premises used: le_inf_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
pos : ∀ (d : α) (ds : d ∈ s) (cd : c ≤ d), c ≤ ⨆ b ∈ s, a ⊓ b
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩

Premises used: And.right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
d : α
ds : d ∈ s
cd : c ≤ d
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
(le_inf hcinf.1 cd).trans (le_biSup _ ds)

Premises used: le_inf, And.left, LE.le.trans, le_biSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
d : α
ds : d ∈ s
cd : c ≤ d
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
exact (le_inf hcinf.1 cd).trans (le_biSup _ ds)

Premises used: le_inf, And.left, LE.le.trans, le_biSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : ¬s.Nonempty
⊢ s = ∅

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at hs

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s = ∅
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
simp [hs]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
simp_rw : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
⊢ sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a

Tactic:
simp_rw [inf_comm _ a, h.inf_sSup_eq]

Premises used: inf_comm, DirectedOn.inf_sSup_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
rw : a ⊓ sSup (range fun (i : ι) ↦ f i) = ⨆ (i : ι), a ⊓ f i
rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ range f, a ⊓ b) (⨆ (i : ι), a ⊓ f i)
rw₂ rw₃ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), a ⊓ f i) (⨆ (i : ι), a ⊓ f i)
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i

Tactic:
rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]

Premises used: iSup, Directed.directedOn_range, iSup_range, DirectedOn.inf_sSup_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ range f, b ⊓ a) (⨆ (i : ι), f i ⊓ a)
rw₂ rw₃ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), f i ⊓ a) (⨆ (i : ι), f i ⊓ a)
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a

Tactic:
rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]

Premises used: iSup, Directed.directedOn_range, DirectedOn.sSup_inf_eq, iSup_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
simp_rw : a ⊓ sSup s = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → a ⊓ b = ⊥
simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → a ⊓ b = ⊥
⊢ Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b

Tactic:
simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]

Premises used: disjoint_iff, DirectedOn.inf_sSup_eq, iSup_eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
simp_rw : sSup s ⊓ a = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → b ⊓ a = ⊥
simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, b ⊓ a) ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → b ⊓ a = ⊥
⊢ Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a

Tactic:
simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]

Premises used: DirectedOn.sSup_inf_eq, disjoint_iff, iSup_eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
simp_rw : a ⊓ ⨆ (i : ι), f i = ⊥ ↔ ∀ (i : ι), a ⊓ f i = ⊥
simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), a ⊓ f i) ⊥ ↔ ∀ (i : ι), a ⊓ f i = ⊥
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)

Tactic:
simp_rw [disjoint_iff, h.inf_iSup_eq, iSup_eq_bot]

Premises used: disjoint_iff, Directed.inf_iSup_eq, iSup_eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
simp_rw : (⨆ (i : ι), f i) ⊓ a = ⊥ ↔ ∀ (i : ι), f i ⊓ a = ⊥
simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), f i ⊓ a) ⊥ ↔ ∀ (i : ι), f i ⊓ a = ⊥
⊢ Disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), Disjoint (f i) a

Tactic:
simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]

Premises used: disjoint_iff, Directed.iSup_inf_eq, iSup_eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
rw : ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
⊢ a ⊓ sSup s ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id

Tactic:
rw [le_iff_compact_le_imp]

Premises used: le_iff_compact_le_imp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id

Tactic:
rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at hc

Premises used: CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
hc₁ : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
⊢ c ≤ a ⊓ sSup s

Tactic:
rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at hc

Premises used: CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ a ∧ c ≤ sSup s

Tactic:
rw [le_inf_iff] at hcinf

Premises used: le_inf_iff