-- Mathlib/Order/Atoms.lean
theorem CompleteLattice.isStronglyAtomic [IsUpperModularLattice α] [IsAtomistic α] :
    IsStronglyAtomic α where
  exists_covBy_le_of_lt a b hab

Proof state:
case intro.intro.inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
h_inf : x ⊓ a = x
⊢ x ≤ a

Tactic:
rwa [inf_eq_left] at h_inf

Result:
no goals

Proof state:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ⊓ a ≤ x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ ⊥ ≤ x ⊓ a

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
hcon : ¬∃ x, a ⋖ x ∧ x ≤ sSup s
x : α
hx : x ∈ s
⊢ x ≤ a

Tactic:
simp_rw [not_exists, and_comm (b := _ ≤ _), not_and] at hcon

Result:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ∀ x ≤ sSup s, ¬a ⋖ x
⊢ x ≤ a

Proof state:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ∀ x ≤ sSup s, ¬a ⋖ x
⊢ x ≤ a

Tactic:
specialize hcon (x ⊔ a) (sup_le (le_sSup _ _ hx) hab.le)

Result:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ≤ a

Proof state:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
⊢ ∃ x, a ⋖ x ∧ x ≤ sSup s

Tactic:
refine by_contra fun hcon ↦ hab.not_le <| sSup_le_iff.2 fun x hx ↦ ?_

Result:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
hcon : ¬∃ x, a ⋖ x ∧ x ≤ sSup s
x : α
hx : x ∈ s
⊢ x ≤ a

Proof state:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ≤ a

Tactic:
obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)

Result:
case intro.intro.inl
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
hbot : x ⊓ a = ⊥
⊢ x ≤ a

case intro.intro.inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
h_inf : x ⊓ a = x
⊢ x ≤ a

Proof state:
case intro.intro.inl
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
hbot : x ⊓ a = ⊥
⊢ x ≤ a

Tactic:
exact False.elim <| hcon <|
  (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy

Result:
no goals

Proof state:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨s, rfl, h⟩ := eq_sSup_atoms b

Result:
case intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a : α
s : Set α
h : ∀ a ∈ s, IsAtom a
hab : a < sSup s
⊢ ∃ x, a ⋖ x ∧ x ≤ sSup s