-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem DirectedOn.inf_sSup_eq (h : DirectedOn (· ≤ ·) s) : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
  le_antisymm
    (by
      rw [le_iff_compact_le_imp]
      by_cases hs : s.Nonempty
      · intro c hc hcinf
        rw [le_inf_iff] at hcinf
        rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc
        rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩
        refine (le_inf hcinf.1 cd).trans (le_trans ?_ (le_iSup₂ d ds))
        rfl
      · rw [Set.not_nonempty_iff_eq_empty] at hs
        simp [hs])
    iSup_inf_le_inf_sSup

Proof state:
case pos.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : 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:
refine (le_inf hcinf.1 cd).trans (le_trans ?_ (le_iSup₂ d ds))

Result:
case pos.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : 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
⊢ a ⊓ d ≤ a ⊓ d

Proof state:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s.Nonempty
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
intro c hc hcinf

Result:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Proof state:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [le_inf_iff] at hcinf

Result:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Proof state:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc

Result:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : 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
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Proof state:
case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : ¬s.Nonempty
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at hs

Result:
case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s = ∅
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [le_iff_compact_le_imp]

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
by_cases hs : s.Nonempty

Result:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s.Nonempty
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : ¬s.Nonempty
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Proof state:
case pos.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : 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
⊢ a ⊓ d ≤ a ⊓ d

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : 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
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

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

Result:
case pos.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : 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

Proof state:
case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hs : s = ∅
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
simp [hs]

Result:
no goals