[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a✝ b✝ x a b : α
⊢ b < a → b = ⊥ ↔ b ≠ ⊥ → b ≤ a → a ≤ b
[PROOFSTEP]
simp only [Ne.def, @not_imp_comm (b = ⊥), not_imp, lt_iff_le_not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b x : α
h : IsAtom a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a
[PROOFSTEP]
rw [le_iff_lt_or_eq, h.lt_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b x : α
⊢ ⊥ ⋖ a ↔ IsAtom a
[PROOFSTEP]
simp only [Covby, bot_lt_iff_ne_bot, IsAtom, not_imp_not]
[GOAL]
α : Type u_1
β : Type u_2
a : α
ι : Sort u_3
inst✝ : Order.Frame α
ha : IsAtom a
f : ι → α
⊢ a ≤ iSup f ↔ ∃ i, a ≤ f i
[PROOFSTEP]
refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩
[GOAL]
α : Type u_1
β : Type u_2
a : α
ι : Sort u_3
inst✝ : Order.Frame α
ha : IsAtom a
f : ι → α
⊢ a ≤ iSup f → ∃ i, a ≤ f i
[PROOFSTEP]
show (a ≤ ⨆ i, f i) → _
[GOAL]
α : Type u_1
β : Type u_2
a : α
ι : Sort u_3
inst✝ : Order.Frame α
ha : IsAtom a
f : ι → α
⊢ a ≤ ⨆ (i : ι), f i → ∃ i, a ≤ f i
[PROOFSTEP]
refine fun h => of_not_not fun ha' => ?_
[GOAL]
α : Type u_1
β : Type u_2
a : α
ι : Sort u_3
inst✝ : Order.Frame α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ (i : ι), f i
ha' : ¬∃ i, a ≤ f i
⊢ False
[PROOFSTEP]
push_neg at ha'
[GOAL]
α : Type u_1
β : Type u_2
a : α
ι : Sort u_3
inst✝ : Order.Frame α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
⊢ False
[PROOFSTEP]
have ha'' : Disjoint a (⨆ i, f i) :=
  disjoint_iSup_iff.2 fun i => fun x hxa hxf =>
    le_bot_iff.2 <|
      of_not_not fun hx =>
        have hxa : x < a := (le_iff_eq_or_lt.1 hxa).resolve_left (by rintro rfl; exact ha' _ hxf)
        hx (ha.2 _ hxa)
[GOAL]
α : Type u_1
β : Type u_2
a : α
ι : Sort u_3
inst✝ : Order.Frame α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
i : ι
x : α
hxa : x ≤ a
hxf : x ≤ f i
hx : ¬x = ⊥
⊢ ¬x = a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝ : Order.Frame α
f : ι → α
i : ι
x : α
hxf : x ≤ f i
hx : ¬x = ⊥
ha : IsAtom x
h : x ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬x ≤ f i
hxa : x ≤ x
⊢ False
[PROOFSTEP]
exact ha' _ hxf
[GOAL]
α : Type u_1
β : Type u_2
a : α
ι : Sort u_3
inst✝ : Order.Frame α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
⊢ False
[PROOFSTEP]
obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝ : Order.Frame α
f : ι → α
ha : IsAtom ⊥
h : ⊥ ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬⊥ ≤ f i
ha'' : Disjoint ⊥ (⨆ (i : ι), f i)
⊢ False
[PROOFSTEP]
exact ha.1 rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ IsAtom b ↔ a ⋖ ↑b
[PROOFSTEP]
rw [← bot_covby_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ ⊥ ⋖ b ↔ a ⋖ ↑b
[PROOFSTEP]
refine' (Set.OrdConnected.apply_covby_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) _).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ OrdConnected (range ↑(OrderEmbedding.subtype fun c => a ≤ c))
[PROOFSTEP]
simpa only [OrderEmbedding.subtype_apply, Subtype.range_coe_subtype] using Set.ordConnected_Ici
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ IsCoatom a ↔ ↑a ⋖ b
[PROOFSTEP]
rw [← covby_top_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b
[PROOFSTEP]
refine' (Set.OrdConnected.apply_covby_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) _).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ OrdConnected (range ↑(OrderEmbedding.subtype fun c => c ≤ b))
[PROOFSTEP]
simpa only [OrderEmbedding.subtype_apply, Subtype.range_coe_subtype] using Set.ordConnected_Iic
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsAtom { val := b, property := h }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsCoatom { val := a, property := h }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsCoatomic αᵒᵈ
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
apply h.eq_top_or_exists_le_coatom
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomic α
b : αᵒᵈ
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
apply h.eq_bot_or_exists_atom_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsAtomic αᵒᵈ
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
apply h.eq_bot_or_exists_atom_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsCoatomic α
b : αᵒᵈ
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
apply h.eq_top_or_exists_le_coatom
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
⊢ x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
[PROOFSTEP]
refine ⟨fun h a _ => (le_trans · h), fun h => ?_⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
⊢ x ≤ y
[PROOFSTEP]
have : x ⊓ yᶜ = ⊥ :=
  of_not_not fun hbot =>
    have ⟨a, ha, hle⟩ := (eq_bot_or_exists_atom_le _).resolve_left hbot
    have ⟨hx, hy'⟩ := le_inf_iff.1 hle
    have hy := h a ha hx
    have : a ≤ y ⊓ yᶜ := le_inf_iff.2 ⟨hy, hy'⟩
    ha.1 (by simpa using this)
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
hbot : ¬x ⊓ yᶜ = ⊥
a : α
ha : IsAtom a
hle : a ≤ x ⊓ yᶜ
hx : a ≤ x
hy' : a ≤ yᶜ
hy : a ≤ y
this : a ≤ y ⊓ yᶜ
⊢ a = ⊥
[PROOFSTEP]
simpa using this
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ x ≤ y
[PROOFSTEP]
exact (eq_compl_iff_isCompl.1 (by simp)).inf_right_eq_bot_iff.1 this
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ y = yᶜᶜ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
⊢ x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
[PROOFSTEP]
refine ⟨fun h => h ▸ by simp, fun h => ?_⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : x = y
⊢ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ x)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
⊢ x = y
[PROOFSTEP]
exact
  le_antisymm (le_iff_atom_le_imp.2 fun a ha hx => (h a ha).1 hx) (le_iff_atom_le_imp.2 fun a ha hy => (h a ha).2 hy)
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type ?u.23945
inst✝¹ : CompleteBooleanAlgebra α
inst✝ : IsAtomic α
src✝ : CompleteBooleanAlgebra α := inst✝¹
ι✝ : Type ?u.23945
κ✝ : ι✝ → Type ?u.23945
f : (a : ι✝) → κ✝ a → α
a : α
ha : IsAtom a
⊢ a ≤ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b ↔ a ≤ ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)
[PROOFSTEP]
simp only [le_iInf_iff, atom_le_iSup ha]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : PartialOrder α✝
α : Type ?u.23945
inst✝¹ : CompleteBooleanAlgebra α
inst✝ : IsAtomic α
src✝ : CompleteBooleanAlgebra α := inst✝¹
ι✝ : Type ?u.23945
κ✝ : ι✝ → Type ?u.23945
f : (a : ι✝) → κ✝ a → α
a : α
ha : IsAtom a
⊢ (∀ (i : ι✝), ∃ i_1, a ≤ f i i_1) ↔ ∃ i, ∀ (i_1 : ι✝), a ≤ f i_1 (i i_1)
[PROOFSTEP]
rw [Classical.skolem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
h : IsCoatomistic αᵒᵈ
b : α
⊢ ∃ s, b = sSup s ∧ ∀ (a : α), a ∈ s → IsAtom a
[PROOFSTEP]
apply h.eq_sInf_coatoms
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
h : IsAtomistic α
b : αᵒᵈ
⊢ ∃ s, b = sInf s ∧ ∀ (a : αᵒᵈ), a ∈ s → IsCoatom a
[PROOFSTEP]
apply h.eq_sSup_atoms
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
h : IsAtomistic αᵒᵈ
b : α
⊢ ∃ s, b = sInf s ∧ ∀ (a : α), a ∈ s → IsCoatom a
[PROOFSTEP]
apply h.eq_sSup_atoms
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
h : IsCoatomistic α
b : αᵒᵈ
⊢ ∃ s, b = sSup s ∧ ∀ (a : αᵒᵈ), a ∈ s → IsAtom a
[PROOFSTEP]
apply h.eq_sInf_coatoms
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
rcases eq_sSup_atoms b with ⟨s, rfl, hs⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsAtom a
⊢ sSup s = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ sSup s
[PROOFSTEP]
cases' s.eq_empty_or_nonempty with h h
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsAtom a
h : s = ∅
⊢ sSup s = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ sSup s
[PROOFSTEP]
simp [h]
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsAtom a
h : Set.Nonempty s
⊢ sSup s = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ sSup s
[PROOFSTEP]
exact Or.intro_right _ ⟨h.some, hs _ h.choose_spec, le_sSup h.choose_spec⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
b : α
⊢ sSup {a | IsAtom a ∧ a ≤ b} = b
[PROOFSTEP]
rcases eq_sSup_atoms b with ⟨s, rfl, hs⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsAtom a
⊢ sSup {a | IsAtom a ∧ a ≤ sSup s} = sSup s
[PROOFSTEP]
exact le_antisymm (sSup_le fun _ => And.right) (sSup_le_sSup fun a ha => ⟨hs a ha, le_sSup ha⟩)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
⊢ sSup {a | IsAtom a} = ⊤
[PROOFSTEP]
refine' Eq.trans (congr rfl (Set.ext fun x => _)) (sSup_atoms_le_eq ⊤)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
x : α
⊢ x ∈ {a | IsAtom a} ↔ x ∈ {a | IsAtom a ∧ a ≤ ⊤}
[PROOFSTEP]
exact (and_iff_left le_top).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ a ≤ b
[PROOFSTEP]
rw [← sSup_atoms_le_eq a, ← sSup_atoms_le_eq b]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ sSup {a_1 | IsAtom a_1 ∧ a_1 ≤ a} ≤ sSup {a | IsAtom a ∧ a ≤ b}
[PROOFSTEP]
exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
⊢ a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
[PROOFSTEP]
refine ⟨fun h => h ▸ by simp, fun h => ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : a = b
⊢ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a = b
[PROOFSTEP]
exact
  le_antisymm (le_iff_atom_le_imp.2 fun a ha hx => (h a ha).1 hx) (le_iff_atom_le_imp.2 fun a ha hy => (h a ha).2 hy)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomistic α
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
rcases eq_sInf_coatoms b with ⟨s, rfl, hs⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsCoatom a
⊢ sInf s = ⊤ ∨ ∃ a, IsCoatom a ∧ sInf s ≤ a
[PROOFSTEP]
cases' s.eq_empty_or_nonempty with h h
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsCoatom a
h : s = ∅
⊢ sInf s = ⊤ ∨ ∃ a, IsCoatom a ∧ sInf s ≤ a
[PROOFSTEP]
simp [h]
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsCoatom a
h : Set.Nonempty s
⊢ sInf s = ⊤ ∨ ∃ a, IsCoatom a ∧ sInf s ≤ a
[PROOFSTEP]
exact Or.intro_right _ ⟨h.some, hs _ h.choose_spec, sInf_le h.choose_spec⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
⊢ ∃ s, b = sSup s ∧ ∀ (a : α), a ∈ s → IsAtom a
[PROOFSTEP]
inhabit α
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∃ s, b = sSup s ∧ ∀ (a : α), a ∈ s → IsAtom a
[PROOFSTEP]
refine ⟨{a | IsAtom a ∧ a ≤ b}, ?_, fun a ha => ha.1⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b = sSup {a | IsAtom a ∧ a ≤ b}
[PROOFSTEP]
refine le_antisymm ?_ (sSup_le fun c hc => hc.2)
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b ≤ sSup {a | IsAtom a ∧ a ≤ b}
[PROOFSTEP]
have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq, iInf_const]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b
[PROOFSTEP]
simp [iSup_bool_eq, iInf_const]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b
⊢ b ≤ sSup {a | IsAtom a ∧ a ≤ b}
[PROOFSTEP]
rw [← this]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b
⊢ (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ}
[PROOFSTEP]
clear this
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ}
[PROOFSTEP]
simp_rw [iInf_iSup_eq, iSup_le_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∀ (i : α → Bool),
    (⨅ (a : α), b ⊓ bif i a then a else aᶜ) ≤
      sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
[PROOFSTEP]
intro g
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
[PROOFSTEP]
by_cases (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
[PROOFSTEP]
by_cases (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : (⨅ (a : α), b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
case neg
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ (a : α), b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
[PROOFSTEP]
case pos => simp [h]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : (⨅ (a : α), b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
[PROOFSTEP]
case pos => simp [h]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : (⨅ (a : α), b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ (a : α), b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤
    sSup {a | IsAtom a ∧ a ≤ ⨆ (g : α → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ}
[PROOFSTEP]
refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ (a : α), b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ≤ ⨅ (a : α), b ⊓ bif g a then a else aᶜ
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ (a : α), b ⊓ bif g a then a else aᶜ) = ⊥
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
⊢ c = ⊥
[PROOFSTEP]
clear h
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
⊢ c = ⊥
[PROOFSTEP]
have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
this : c < bif g c then c else cᶜ
⊢ c = ⊥
[PROOFSTEP]
revert this
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
⊢ (c < bif g c then c else cᶜ) → c = ⊥
[PROOFSTEP]
nontriviality α
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
✝ : Nontrivial α
⊢ (c < bif g c then c else cᶜ) → c = ⊥
[PROOFSTEP]
cases g c
[GOAL]
case false
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
✝ : Nontrivial α
⊢ (c < bif false then c else cᶜ) → c = ⊥
[PROOFSTEP]
simp
[GOAL]
case true
α✝ : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α✝
α : Type ?u.31123
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
✝ : Nontrivial α
⊢ (c < bif true then c else cᶜ) → c = ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α → IsSimpleOrder αᵒᵈ
[PROOFSTEP]
intro i
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder αᵒᵈ → IsSimpleOrder α
[PROOFSTEP]
intro i
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ
[PROOFSTEP]
haveI := i
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α
[PROOFSTEP]
haveI := i
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ
[PROOFSTEP]
exact
  { exists_pair_ne := @exists_pair_ne α _
    eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α
[PROOFSTEP]
exact
  { exists_pair_ne := @exists_pair_ne αᵒᵈ _
    eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
obtain ⟨a, b, h⟩ := exists_pair_ne α
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
h : a ≠ b
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
rcases eq_bot_or_eq_top a with (rfl | rfl)
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : ⊥ ≠ b
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
rcases eq_bot_or_eq_top b with (rfl | rfl)
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : ⊤ ≠ b
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
rcases eq_bot_or_eq_top b with (rfl | rfl)
[GOAL]
case intro.intro.inl.inl
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
first
| simpa
| simpa using h.symm
[GOAL]
case intro.intro.inl.inl
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.inl.inl
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
simpa using h.symm
[GOAL]
case intro.intro.inl.inr
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊤
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
first
| simpa
| simpa using h.symm
[GOAL]
case intro.intro.inl.inr
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊤
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
first
| simpa
| simpa using h.symm
[GOAL]
case intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.inr.inl
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
simpa using h.symm
[GOAL]
case intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
first
| simpa
| simpa using h.symm
[GOAL]
case intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.inr.inr
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
simpa using h.symm
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47226
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsSimpleOrder α
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a : α
⊢ a ≤ a
[PROOFSTEP]
rcases eq_bot_or_eq_top a with (rfl | rfl)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≤ ⊥
[PROOFSTEP]
simp
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊤
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b c : α
⊢ a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
rcases eq_bot_or_eq_top a with (rfl | rfl)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊥ ≤ b → b ≤ c → ⊥ ≤ c
[PROOFSTEP]
simp
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c
[PROOFSTEP]
rcases eq_bot_or_eq_top b with (rfl | rfl)
[GOAL]
case inr.inl
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ c → ⊤ ≤ c
[PROOFSTEP]
rcases eq_bot_or_eq_top c with (rfl | rfl)
[GOAL]
case inr.inl.inl
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊥ → ⊤ ≤ ⊥
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊤ → ⊤ ≤ ⊤
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α✝ : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.47699
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ c → ⊤ ≤ c
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
src✝ : PartialOrder α := inferInstance
a b : α
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
rcases eq_bot_or_eq_top a with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
src✝ : PartialOrder α := inferInstance
b : α
⊢ ⊥ ≤ b ∨ b ≤ ⊥
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
src✝ : PartialOrder α := inferInstance
b : α
⊢ ⊤ ≤ b ∨ b ≤ ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : Lattice α := inferInstance
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : Lattice α := inferInstance
y z : α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : Lattice α := inferInstance
y z : α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsAtomic αᵒᵈ
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.66638
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ (fun x => bif x then ⊤ else ⊥) ((fun x => decide (x = ⊤)) x) = x
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.66638
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x => bif x then ⊤ else ⊥) ((fun x => decide (x = ⊤)) ⊥) = ⊥
[PROOFSTEP]
simp [bot_ne_top]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.66638
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x => bif x then ⊤ else ⊥) ((fun x => decide (x = ⊤)) ⊤) = ⊤
[PROOFSTEP]
simp [bot_ne_top]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.66638
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : Bool
⊢ (fun x => decide (x = ⊤)) ((fun x => bif x then ⊤ else ⊥) x) = x
[PROOFSTEP]
cases x
[GOAL]
case false
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.66638
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x => decide (x = ⊤)) ((fun x => bif x then ⊤ else ⊥) false) = false
[PROOFSTEP]
simp [bot_ne_top]
[GOAL]
case true
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.66638
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x => decide (x = ⊤)) ((fun x => bif x then ⊤ else ⊥) true) = true
[PROOFSTEP]
simp [bot_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : α ≃ Bool := equivBool
a b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        a ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    a ≤ b
[PROOFSTEP]
rcases eq_bot_or_eq_top a with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : α ≃ Bool := equivBool
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ⊥ ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    ⊥ ≤ b
[PROOFSTEP]
simp [bot_ne_top]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : α ≃ Bool := equivBool
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ⊤ ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    ⊤ ≤ b
[PROOFSTEP]
rcases eq_bot_or_eq_top b with (rfl | rfl)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : α ≃ Bool := equivBool
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ⊤ ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ⊥ ↔
    ⊤ ≤ ⊥
[PROOFSTEP]
simp [bot_ne_top.symm, bot_ne_top, Bool.false_lt_true]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝ : α ≃ Bool := equivBool
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ⊤ ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ⊤ ↔
    ⊤ ≤ ⊤
[PROOFSTEP]
simp [bot_ne_top]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
x : α
⊢ x ⊓ xᶜ ≤ ⊥
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
⊢ ⊥ ⊓ ⊥ᶜ ≤ ⊥
[PROOFSTEP]
simp
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
⊢ ⊤ ⊓ ⊤ᶜ ≤ ⊥
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
x : α
⊢ ⊤ ≤ x ⊔ xᶜ
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
⊢ ⊤ ≤ ⊥ ⊔ ⊥ᶜ
[PROOFSTEP]
simp
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
⊢ ⊤ ≤ ⊤ ⊔ ⊤ᶜ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
x y : α
⊢ x \ y = x ⊓ yᶜ
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
y : α
⊢ ⊥ \ y = ⊥ ⊓ yᶜ
[PROOFSTEP]
simp [bot_ne_top, SDiff.sdiff, compl]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.72459
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : BoundedOrder α := inferInstanceAs (BoundedOrder α)
src✝ : DistribLattice α := IsSimpleOrder.distribLattice
y : α
⊢ ⊤ \ y = ⊤ ⊓ yᶜ
[PROOFSTEP]
simp [bot_ne_top, SDiff.sdiff, compl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
x : α
h : x ∈ s
⊢ x ≤ sSup s
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ⊥ ∈ s
⊢ ⊥ ≤ sSup s
[PROOFSTEP]
exact bot_le
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ⊤ ∈ s
⊢ ⊤ ≤ sSup s
[PROOFSTEP]
dsimp
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ⊤ ∈ s
⊢ ⊤ ≤ if ⊤ ∈ s then ⊤ else ⊥
[PROOFSTEP]
rw [if_pos h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
x : α
h : ∀ (b : α), b ∈ s → b ≤ x
⊢ sSup s ≤ x
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → b ≤ ⊥
⊢ sSup s ≤ ⊥
[PROOFSTEP]
dsimp
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → b ≤ ⊥
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊥
[PROOFSTEP]
rw [if_neg]
[GOAL]
case inl.hnc
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → b ≤ ⊥
⊢ ¬⊤ ∈ s
[PROOFSTEP]
intro con
[GOAL]
case inl.hnc
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → b ≤ ⊥
con : ⊤ ∈ s
⊢ False
[PROOFSTEP]
exact bot_ne_top (eq_top_iff.2 (h ⊤ con))
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → b ≤ ⊤
⊢ sSup s ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
x : α
h : x ∈ s
⊢ sInf s ≤ x
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ⊥ ∈ s
⊢ sInf s ≤ ⊥
[PROOFSTEP]
dsimp
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ⊥ ∈ s
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ ⊥
[PROOFSTEP]
rw [if_pos h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ⊤ ∈ s
⊢ sInf s ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
x : α
h : ∀ (b : α), b ∈ s → x ≤ b
⊢ x ≤ sInf s
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → ⊥ ≤ b
⊢ ⊥ ≤ sInf s
[PROOFSTEP]
exact bot_le
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → ⊤ ≤ b
⊢ ⊤ ≤ sInf s
[PROOFSTEP]
dsimp
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → ⊤ ≤ b
⊢ ⊤ ≤ if ⊥ ∈ s then ⊥ else ⊤
[PROOFSTEP]
rw [if_neg]
[GOAL]
case inr.hnc
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → ⊤ ≤ b
⊢ ¬⊥ ∈ s
[PROOFSTEP]
intro con
[GOAL]
case inr.hnc
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : Lattice α := inferInstance
src✝ : BoundedOrder α := inferInstance
s : Set α
h : ∀ (b : α), b ∈ s → ⊤ ≤ b
con : ⊥ ∈ s
⊢ False
[PROOFSTEP]
exact top_ne_bot (eq_bot_iff.2 (h ⊥ con))
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
x : α
s : Set α
⊢ x ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), x ⊓ b
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
s : Set α
⊢ ⊥ ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), ⊥ ⊓ b
[PROOFSTEP]
simp only [le_bot_iff, sSup_eq_bot, bot_inf_eq, iSup_bot, le_refl]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
s : Set α
⊢ ⊤ ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), ⊤ ⊓ b
[PROOFSTEP]
simp only [top_inf_eq, ← sSup_eq_iSup]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
s : Set α
⊢ sSup s ≤ sSup s
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
x : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), x ⊔ b ≤ x ⊔ sInf s
[PROOFSTEP]
rcases eq_bot_or_eq_top x with (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), ⊥ ⊔ b ≤ ⊥ ⊔ sInf s
[PROOFSTEP]
simp only [bot_sup_eq, ← sInf_eq_iInf]
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
s : Set α
⊢ sInf s ≤ sInf s
[PROOFSTEP]
exact le_rfl
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
src✝¹ : CompleteLattice α := IsSimpleOrder.completeLattice
src✝ : BooleanAlgebra α := IsSimpleOrder.booleanAlgebra
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), ⊤ ⊔ b ≤ ⊤ ⊔ sInf s
[PROOFSTEP]
simp only [top_le_iff, top_sup_eq, iInf_top, le_sInf_iff, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsSimpleOrder α
⊢ IsAtomistic αᵒᵈ
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : ↑f ⊥ = ⊥
b : β
hb : IsAtom (↑f b)
⊢ IsAtom b
[PROOFSTEP]
simp only [← bot_covby_iff] at hb ⊢
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : ↑f ⊥ = ⊥
b : β
hb : ⊥ ⋖ ↑f b
⊢ ⊥ ⋖ b
[PROOFSTEP]
exact Covby.of_image f (hbot.symm ▸ hb)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
⊢ IsAtom (l a) ↔ IsAtom a
[PROOFSTEP]
refine' ⟨fun hla => _, fun ha => gi.isAtom_of_u_bot hbot ((h_atom a ha).symm ▸ ha)⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
⊢ IsAtom a
[PROOFSTEP]
obtain ⟨a', ha', hab'⟩ := (eq_bot_or_exists_atom_le (u (l a))).resolve_left (hbot ▸ fun h => hla.1 (gi.u_injective h))
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
⊢ IsAtom a
[PROOFSTEP]
have :=
  (hla.le_iff.mp <| (gi.l_u_eq (l a) ▸ gi.gc.monotone_l hab' : l a' ≤ l a)).resolve_left fun h =>
    ha'.1 (hbot ▸ h_atom a' ha' ▸ congr_arg u h)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
this : l a' = l a
⊢ IsAtom a
[PROOFSTEP]
have haa' : a = a' :=
  (ha'.le_iff.mp <| (gi.gc.le_u_l a).trans_eq (h_atom a' ha' ▸ congr_arg u this.symm)).resolve_left
    (mt (congr_arg l) (gi.gc.l_bot.symm ▸ hla.1))
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
this : l a' = l a
haa' : a = a'
⊢ IsAtom a
[PROOFSTEP]
exact haa'.symm ▸ ha'
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom (u b) ↔ IsAtom b
[PROOFSTEP]
rw [← gi.isAtom_iff hbot h_atom, gi.l_u_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b
[PROOFSTEP]
refine' ⟨fun hb => gi.isCoatom_of_image hb, fun hb => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
⊢ IsCoatom (u b)
[PROOFSTEP]
obtain ⟨a, ha, hab⟩ :=
  (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
    hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
⊢ IsCoatom (u b)
[PROOFSTEP]
have : l a = b :=
  (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
    ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
this : l a = b
⊢ IsCoatom (u b)
[PROOFSTEP]
exact this ▸ (h_coatom a ha).symm ▸ ha
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsSimpleOrder α ↔ IsSimpleOrder β
[PROOFSTEP]
rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤, f.map_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : α ≃o β
⊢ IsAtomic α ↔ IsAtomic β
[PROOFSTEP]
simp only [IsAtomic_iff, f.surjective.forall, f.surjective.exists, ← map_bot f, f.eq_iff_eq, f.le_iff_le, f.isAtom_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderTop α
inst✝ : OrderTop β
f : α ≃o β
⊢ IsCoatomic α ↔ IsCoatomic β
[PROOFSTEP]
simp only [← isAtomic_dual_iff_isCoatomic, f.dual.isAtomic_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x : α
⊢ x = ⊤ ∨ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
rcases exists_isCompl x with ⟨y, xy⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
⊢ x = ⊤ ∨ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
apply (eq_bot_or_exists_atom_le y).imp _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
⊢ y = ⊥ → x = ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x : α
xy : IsCompl x ⊥
⊢ x = ⊤
[PROOFSTEP]
exact eq_top_of_isCompl_bot xy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
⊢ (∃ a, IsAtom a ∧ a ≤ y) → ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
rintro ⟨a, ha, ay⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
rcases exists_isCompl (xy.symm.IicOrderIsoIci ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩
[GOAL]
case intro.intro.intro.mk
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (↑(IsCompl.IicOrderIsoIci (_ : IsCompl y x)) { val := a, property := ay }) { val := b, property := xb }
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
refine' ⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici _, xb⟩
[GOAL]
case intro.intro.intro.mk
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (↑(IsCompl.IicOrderIsoIci (_ : IsCompl y x)) { val := a, property := ay }) { val := b, property := xb }
⊢ IsCoatom { val := b, property := xb }
[PROOFSTEP]
rw [← hb.isAtom_iff_isCoatom, OrderIso.isAtom_iff]
[GOAL]
case intro.intro.intro.mk
α : Type u_1
β : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (↑(IsCompl.IicOrderIsoIci (_ : IsCompl y x)) { val := a, property := ay }) { val := b, property := xb }
⊢ IsAtom { val := a, property := ay }
[PROOFSTEP]
apply ha.Iic
[GOAL]
α : Type u_1
β : Type u_2
p : Prop
⊢ IsAtom p ↔ p
[PROOFSTEP]
simp [IsAtom, show ⊥ = False from rfl, fun q r : Prop => show q < r ↔ _ ∧ _ from .rfl]
[GOAL]
α : Type u_1
β : Type u_2
p : Prop
⊢ IsCoatom p ↔ ¬p
[PROOFSTEP]
simp [IsCoatom, show ⊤ = True from rfl, fun q r : Prop => show q < r ↔ _ ∧ _ from .rfl]
[GOAL]
α : Type u_1
β : Type u_2
p : Prop
⊢ ¬p → ∀ (b : Prop), (p → b) → b → ¬p → b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
p : Prop
⊢ p = ⊥ ∨ p = ⊤
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
β : Type u_2
p : Prop
⊢ p = ⊥ ∨ p = ⊤
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
β : Type u_2
p : Prop
h : p
⊢ p = ⊥ ∨ p = ⊤
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
p : Prop
h : ¬p
⊢ p = ⊥ ∨ p = ⊤
[PROOFSTEP]
simp [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
p : Prop
h : p
⊢ ⊥ ∨ ⊤
[PROOFSTEP]
tauto
[GOAL]
case neg
α : Type u_1
β : Type u_2
p : Prop
h : ¬p
⊢ ¬⊥ ∨ ¬⊤
[PROOFSTEP]
tauto
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝ : (i : ι) → Bot (π i)
f : (i : ι) → π i
h : ∀ (i : ι), f i = ⊥
i : ι
⊢ f i = ⊥ i
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
classical
constructor
case mpr =>
  rintro ⟨i, ⟨hfi, hlt⟩, hbot⟩
  refine ⟨fun h => hfi ((Pi.eq_bot_iff.1 h) _), fun g hgf => Pi.eq_bot_iff.2 fun j => ?_⟩
  have ⟨hgf, k, hgfk⟩ := Pi.lt_def.1 hgf
  obtain rfl : i = k := of_not_not fun hki => by rw [hbot _ (Ne.symm hki)] at hgfk ; simp at hgfk
  by_cases hij : j = i; case pos => subst hij; refine hlt _ hgfk
  refine eq_bot_iff.2 <| le_trans (hgf _) (eq_bot_iff.1 (hbot _ hij))
case mp =>
  rintro ⟨hbot, h⟩
  have ⟨i, hbot⟩ : ∃ i, f i ≠ ⊥ := by rw [ne_eq, Pi.eq_bot_iff, not_forall] at hbot ; exact hbot
  refine ⟨i, ⟨hbot, ?c⟩, ?d⟩
  case c =>
    intro b hb
    have := h (Function.update ⊥ i b)
    simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
    simpa using
      this
        (fun j => by by_cases h : j = i;
          {subst h; simpa using le_of_lt hb
          };
          simp [h])
        i (by simpa using hb) i
  case d =>
    intro j hj
    have := h (Function.update ⊥ j (f j))
    simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
    simpa using
      this
        (fun k => by by_cases k = j;
          {subst h; simp
          };
          simp [h])
        i (by rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f → ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
case mpr
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ (∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥) → IsAtom f
[PROOFSTEP]
case mpr =>
  rintro ⟨i, ⟨hfi, hlt⟩, hbot⟩
  refine ⟨fun h => hfi ((Pi.eq_bot_iff.1 h) _), fun g hgf => Pi.eq_bot_iff.2 fun j => ?_⟩
  have ⟨hgf, k, hgfk⟩ := Pi.lt_def.1 hgf
  obtain rfl : i = k := of_not_not fun hki => by rw [hbot _ (Ne.symm hki)] at hgfk ; simp at hgfk
  by_cases hij : j = i; case pos => subst hij; refine hlt _ hgfk
  refine eq_bot_iff.2 <| le_trans (hgf _) (eq_bot_iff.1 (hbot _ hij))
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ (∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥) → IsAtom f
[PROOFSTEP]
case mpr =>
  rintro ⟨i, ⟨hfi, hlt⟩, hbot⟩
  refine ⟨fun h => hfi ((Pi.eq_bot_iff.1 h) _), fun g hgf => Pi.eq_bot_iff.2 fun j => ?_⟩
  have ⟨hgf, k, hgfk⟩ := Pi.lt_def.1 hgf
  obtain rfl : i = k := of_not_not fun hki => by rw [hbot _ (Ne.symm hki)] at hgfk ; simp at hgfk
  by_cases hij : j = i; case pos => subst hij; refine hlt _ hgfk
  refine eq_bot_iff.2 <| le_trans (hgf _) (eq_bot_iff.1 (hbot _ hij))
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ (∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥) → IsAtom f
[PROOFSTEP]
rintro ⟨i, ⟨hfi, hlt⟩, hbot⟩
[GOAL]
case intro.intro.intro
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
⊢ IsAtom f
[PROOFSTEP]
refine ⟨fun h => hfi ((Pi.eq_bot_iff.1 h) _), fun g hgf => Pi.eq_bot_iff.2 fun j => ?_⟩
[GOAL]
case intro.intro.intro
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf : g < f
j : ι
⊢ g j = ⊥
[PROOFSTEP]
have ⟨hgf, k, hgfk⟩ := Pi.lt_def.1 hgf
[GOAL]
case intro.intro.intro
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
k : ι
hgfk : g k < f k
⊢ g j = ⊥
[PROOFSTEP]
obtain rfl : i = k := of_not_not fun hki => by rw [hbot _ (Ne.symm hki)] at hgfk ; simp at hgfk
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
k : ι
hgfk : g k < f k
hki : ¬i = k
⊢ False
[PROOFSTEP]
rw [hbot _ (Ne.symm hki)] at hgfk
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
k : ι
hgfk : g k < ⊥
hki : ¬i = k
⊢ False
[PROOFSTEP]
simp at hgfk
[GOAL]
case intro.intro.intro
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
⊢ g j = ⊥
[PROOFSTEP]
by_cases hij : j = i
[GOAL]
case pos
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
hij : j = i
⊢ g j = ⊥
case neg
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
hij : ¬j = i
⊢ g j = ⊥
[PROOFSTEP]
case pos => subst hij; refine hlt _ hgfk
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
hij : j = i
⊢ g j = ⊥
[PROOFSTEP]
case pos => subst hij; refine hlt _ hgfk
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
hij : j = i
⊢ g j = ⊥
[PROOFSTEP]
subst hij
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hbot : ∀ (j_1 : ι), j_1 ≠ j → f j_1 = ⊥
hfi : f j ≠ ⊥
hlt : ∀ (b : π j), b < f j → b = ⊥
hgfk : g j < f j
⊢ g j = ⊥
[PROOFSTEP]
refine hlt _ hgfk
[GOAL]
case neg
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ (b : π i), b < f i → b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
hij : ¬j = i
⊢ g j = ⊥
[PROOFSTEP]
refine eq_bot_iff.2 <| le_trans (hgf _) (eq_bot_iff.1 (hbot _ hij))
[GOAL]
case mp
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f → ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
case mp =>
  rintro ⟨hbot, h⟩
  have ⟨i, hbot⟩ : ∃ i, f i ≠ ⊥ := by rw [ne_eq, Pi.eq_bot_iff, not_forall] at hbot ; exact hbot
  refine ⟨i, ⟨hbot, ?c⟩, ?d⟩
  case c =>
    intro b hb
    have := h (Function.update ⊥ i b)
    simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
    simpa using
      this
        (fun j => by by_cases h : j = i;
          {subst h; simpa using le_of_lt hb
          };
          simp [h])
        i (by simpa using hb) i
  case d =>
    intro j hj
    have := h (Function.update ⊥ j (f j))
    simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
    simpa using
      this
        (fun k => by by_cases k = j;
          {subst h; simp
          };
          simp [h])
        i (by rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f → ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
case mp =>
  rintro ⟨hbot, h⟩
  have ⟨i, hbot⟩ : ∃ i, f i ≠ ⊥ := by rw [ne_eq, Pi.eq_bot_iff, not_forall] at hbot ; exact hbot
  refine ⟨i, ⟨hbot, ?c⟩, ?d⟩
  case c =>
    intro b hb
    have := h (Function.update ⊥ i b)
    simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
    simpa using
      this
        (fun j => by by_cases h : j = i;
          {subst h; simpa using le_of_lt hb
          };
          simp [h])
        i (by simpa using hb) i
  case d =>
    intro j hj
    have := h (Function.update ⊥ j (f j))
    simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
    simpa using
      this
        (fun k => by by_cases k = j;
          {subst h; simp
          };
          simp [h])
        i (by rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f → ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
rintro ⟨hbot, h⟩
[GOAL]
case intro
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
⊢ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
have ⟨i, hbot⟩ : ∃ i, f i ≠ ⊥ := by rw [ne_eq, Pi.eq_bot_iff, not_forall] at hbot ; exact hbot
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
⊢ ∃ i, f i ≠ ⊥
[PROOFSTEP]
rw [ne_eq, Pi.eq_bot_iff, not_forall] at hbot
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot : ∃ x, ¬f x = ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
⊢ ∃ i, f i ≠ ⊥
[PROOFSTEP]
exact hbot
[GOAL]
case intro
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
refine ⟨i, ⟨hbot, ?c⟩, ?d⟩
[GOAL]
case c
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (b : π i), b < f i → b = ⊥
case d
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
case c =>
  intro b hb
  have := h (Function.update ⊥ i b)
  simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
  simpa using
    this
      (fun j => by by_cases h : j = i;
        {subst h; simpa using le_of_lt hb
        };
        simp [h])
      i (by simpa using hb) i
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (b : π i), b < f i → b = ⊥
[PROOFSTEP]
case c =>
  intro b hb
  have := h (Function.update ⊥ i b)
  simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
  simpa using
    this
      (fun j => by by_cases h : j = i;
        {subst h; simpa using le_of_lt hb
        };
        simp [h])
      i (by simpa using hb) i
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (b : π i), b < f i → b = ⊥
[PROOFSTEP]
intro b hb
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
⊢ b = ⊥
[PROOFSTEP]
have := h (Function.update ⊥ i b)
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this : Function.update ⊥ i b < f → Function.update ⊥ i b = ⊥
⊢ b = ⊥
[PROOFSTEP]
simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
⊢ b = ⊥
[PROOFSTEP]
simpa using
  this
    (fun j => by by_cases h : j = i;
      {subst h; simpa using le_of_lt hb
      };
      simp [h])
    i (by simpa using hb) i
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
j : ι
⊢ Function.update ⊥ i b j ≤ f j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
j : ι
h : j = i
⊢ Function.update ⊥ i b j ≤ f j
case neg
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
j : ι
h : ¬j = i
⊢ Function.update ⊥ i b j ≤ f j
[PROOFSTEP]
{subst h; simpa using le_of_lt hb
}
[GOAL]
case pos
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
j : ι
h : j = i
⊢ Function.update ⊥ i b j ≤ f j
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
j : ι
hbot : f j ≠ ⊥
b : π j
hb : b < f j
this :
  (∀ (i : ι), Function.update ⊥ j b i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j b x < f x → ∀ (i : ι), Function.update ⊥ j b i = ⊥
⊢ Function.update ⊥ j b j ≤ f j
[PROOFSTEP]
simpa using le_of_lt hb
[GOAL]
case neg
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
j : ι
h : ¬j = i
⊢ Function.update ⊥ i b j ≤ f j
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
⊢ Function.update ⊥ i b i < f i
[PROOFSTEP]
simpa using hb
[GOAL]
case d
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
case d =>
  intro j hj
  have := h (Function.update ⊥ j (f j))
  simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
  simpa using
    this
      (fun k => by by_cases k = j;
        {subst h; simp
        };
        simp [h])
      i (by rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
case d =>
  intro j hj
  have := h (Function.update ⊥ j (f j))
  simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
  simpa using
    this
      (fun k => by by_cases k = j;
        {subst h; simp
        };
        simp [h])
      i (by rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (j : ι), j ≠ i → f j = ⊥
[PROOFSTEP]
intro j hj
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
⊢ f j = ⊥
[PROOFSTEP]
have := h (Function.update ⊥ j (f j))
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this : Function.update ⊥ j (f j) < f → Function.update ⊥ j (f j) = ⊥
⊢ f j = ⊥
[PROOFSTEP]
simp only [lt_def, le_def, ge_iff_le, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
⊢ f j = ⊥
[PROOFSTEP]
simpa using
  this
    (fun k => by by_cases k = j;
      {subst h; simp
      };
      simp [h])
    i (by rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
⊢ Function.update ⊥ j (f j) k ≤ f k
[PROOFSTEP]
by_cases k = j
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
⊢ Function.update ⊥ j (f j) k ≤ f k
[PROOFSTEP]
by_cases k = j
[GOAL]
case pos
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : k = j
⊢ Function.update ⊥ j (f j) k ≤ f k
case neg
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : ¬k = j
⊢ Function.update ⊥ j (f j) k ≤ f k
[PROOFSTEP]
{subst h; simp
}
[GOAL]
case pos
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : k = j
⊢ Function.update ⊥ j (f j) k ≤ f k
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
k : ι
hj : k ≠ i
this :
  (∀ (i : ι), Function.update ⊥ k (f k) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ k (f k) x < f x → ∀ (i : ι), Function.update ⊥ k (f k) i = ⊥
⊢ Function.update ⊥ k (f k) k ≤ f k
[PROOFSTEP]
simp
[GOAL]
case neg
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : ¬k = j
⊢ Function.update ⊥ j (f j) k ≤ f k
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ (b : (i : ι) → π i), b < f → b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
⊢ Function.update ⊥ j (f j) i < f i
[PROOFSTEP]
rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
i : ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
a : π i
h : IsAtom a
⊢ IsAtom (Function.update ⊥ i a i)
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f → ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
case mpr
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f
[PROOFSTEP]
case mp =>
  intro h
  have ⟨i, h, hbot⟩ := isAtom_iff.1 h
  refine ⟨_, _, h, funext fun j => if hij : j = i then hij ▸ by simp else ?_⟩
  rw [Function.update_noteq hij, hbot _ hij, bot_apply]
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f → ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
[PROOFSTEP]
case mp =>
  intro h
  have ⟨i, h, hbot⟩ := isAtom_iff.1 h
  refine ⟨_, _, h, funext fun j => if hij : j = i then hij ▸ by simp else ?_⟩
  rw [Function.update_noteq hij, hbot _ hij, bot_apply]
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f → ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
[PROOFSTEP]
intro h
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h : IsAtom f
⊢ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
[PROOFSTEP]
have ⟨i, h, hbot⟩ := isAtom_iff.1 h
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
⊢ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
[PROOFSTEP]
refine ⟨_, _, h, funext fun j => if hij : j = i then hij ▸ by simp else ?_⟩
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
j : ι
hij : j = i
⊢ f j = Function.update ⊥ j (f j) j
[PROOFSTEP]
simp
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
j : ι
hij : ¬j = i
⊢ f j = Function.update ⊥ i (f i) j
[PROOFSTEP]
rw [Function.update_noteq hij, hbot _ hij, bot_apply]
[GOAL]
case mpr
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f
[PROOFSTEP]
case mpr =>
  rintro ⟨i, a, h, rfl⟩
  refine isAtom_single h
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f
[PROOFSTEP]
case mpr =>
  rintro ⟨i, a, h, rfl⟩
  refine isAtom_single h
[GOAL]
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f
[PROOFSTEP]
rintro ⟨i, a, h, rfl⟩
[GOAL]
case intro.intro.intro
ι : Type u_3
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
a : π i
h : IsAtom a
⊢ IsAtom (Function.update ⊥ i a)
[PROOFSTEP]
refine isAtom_single h
[GOAL]
ι : Type ?u.130792
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomic (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
this : DecidableEq ι
⊢ ∀ (j : ι), j ≠ i → ⊥ j ≤ b j
[PROOFSTEP]
simp
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∃ s_1, s = sSup s_1 ∧ ∀ (a : (i : ι) → π i), a ∈ s_1 → IsAtom a
[PROOFSTEP]
classical
refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp; tauto⟩
ext i
rw [← sSup_atoms_le_eq (s i)]
simp_rw [isAtom_iff_eq_single]
refine le_antisymm ?le ?ge
case le =>
  refine sSup_le fun a ⟨ha, hle⟩ => ?_
  refine le_sSup ⟨⟨_, ⟨_, _, ha, rfl⟩, ?_⟩, by simp⟩
  intro j; by_cases hij : j = i
  case pos => subst hij; simpa
  case neg => simp [hij]
case ge =>
  refine sSup_le ?_
  rintro _ ⟨⟨_, ⟨j, a, ha, rfl⟩, hle⟩, rfl⟩
  by_cases hij : i = j; case neg => simp [Function.update_noteq hij]
  subst hij; simp only [Function.update_same]
  refine le_sSup ⟨ha, by simpa using hle i⟩
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∃ s_1, s = sSup s_1 ∧ ∀ (a : (i : ι) → π i), a ∈ s_1 → IsAtom a
[PROOFSTEP]
refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp; tauto⟩
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∀ (a : (i : ι) → π i), a ∈ {f | IsAtom f ∧ f ≤ s} → IsAtom a
[PROOFSTEP]
simp
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∀ (a : (i : ι) → π i), IsAtom a → a ≤ s → IsAtom a
[PROOFSTEP]
tauto
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ s = sSup {f | IsAtom f ∧ f ≤ s}
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i = sSup {f | IsAtom f ∧ f ≤ s} i
[PROOFSTEP]
rw [← sSup_atoms_le_eq (s i)]
[GOAL]
case h
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {a | IsAtom a ∧ a ≤ s i} = sSup {f | IsAtom f ∧ f ≤ s} i
[PROOFSTEP]
simp_rw [isAtom_iff_eq_single]
[GOAL]
case h
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {a | IsAtom a ∧ a ≤ s i} = sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i
[PROOFSTEP]
refine le_antisymm ?le ?ge
[GOAL]
case le
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {a | IsAtom a ∧ a ≤ s i} ≤ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i
case ge
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i ≤ sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
case le =>
  refine sSup_le fun a ⟨ha, hle⟩ => ?_
  refine le_sSup ⟨⟨_, ⟨_, _, ha, rfl⟩, ?_⟩, by simp⟩
  intro j; by_cases hij : j = i
  case pos => subst hij; simpa
  case neg => simp [hij]
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {a | IsAtom a ∧ a ≤ s i} ≤ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i
[PROOFSTEP]
case le =>
  refine sSup_le fun a ⟨ha, hle⟩ => ?_
  refine le_sSup ⟨⟨_, ⟨_, _, ha, rfl⟩, ?_⟩, by simp⟩
  intro j; by_cases hij : j = i
  case pos => subst hij; simpa
  case neg => simp [hij]
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {a | IsAtom a ∧ a ≤ s i} ≤ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i
[PROOFSTEP]
refine sSup_le fun a ⟨ha, hle⟩ => ?_
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
⊢ a ≤ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i
[PROOFSTEP]
refine le_sSup ⟨⟨_, ⟨_, _, ha, rfl⟩, ?_⟩, by simp⟩
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ i a,
        property :=
          (_ :
            (∃ i_1 a_1, IsAtom a_1 ∧ Function.update ⊥ i a = Function.update ⊥ i_1 a_1) ∧ Function.update ⊥ i a ≤ s) } =
    a
[PROOFSTEP]
simp
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
⊢ Function.update ⊥ i a ≤ s
[PROOFSTEP]
intro j
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
⊢ Function.update ⊥ i a j ≤ s j
[PROOFSTEP]
by_cases hij : j = i
[GOAL]
case pos
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
hij : j = i
⊢ Function.update ⊥ i a j ≤ s j
case neg
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
hij : ¬j = i
⊢ Function.update ⊥ i a j ≤ s j
[PROOFSTEP]
case pos => subst hij; simpa
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
hij : j = i
⊢ Function.update ⊥ i a j ≤ s j
[PROOFSTEP]
case pos => subst hij; simpa
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
hij : j = i
⊢ Function.update ⊥ i a j ≤ s j
[PROOFSTEP]
subst hij
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
j : ι
a : π j
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s j}
ha : IsAtom a
hle : a ≤ s j
⊢ Function.update ⊥ j a j ≤ s j
[PROOFSTEP]
simpa
[GOAL]
case neg
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
hij : ¬j = i
⊢ Function.update ⊥ i a j ≤ s j
[PROOFSTEP]
case neg => simp [hij]
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
hij : ¬j = i
⊢ Function.update ⊥ i a j ≤ s j
[PROOFSTEP]
case neg => simp [hij]
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
x✝ : a ∈ {a | IsAtom a ∧ a ≤ s i}
ha : IsAtom a
hle : a ≤ s i
j : ι
hij : ¬j = i
⊢ Function.update ⊥ i a j ≤ s j
[PROOFSTEP]
simp [hij]
[GOAL]
case ge
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i ≤ sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
case ge =>
  refine sSup_le ?_
  rintro _ ⟨⟨_, ⟨j, a, ha, rfl⟩, hle⟩, rfl⟩
  by_cases hij : i = j; case neg => simp [Function.update_noteq hij]
  subst hij; simp only [Function.update_same]
  refine le_sSup ⟨ha, by simpa using hle i⟩
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i ≤ sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
case ge =>
  refine sSup_le ?_
  rintro _ ⟨⟨_, ⟨j, a, ha, rfl⟩, hle⟩, rfl⟩
  by_cases hij : i = j; case neg => simp [Function.update_noteq hij]
  subst hij; simp only [Function.update_same]
  refine le_sSup ⟨ha, by simpa using hle i⟩
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ sSup {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s} i ≤ sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
refine sSup_le ?_
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ ∀ (b : π i), (b ∈ Set.range fun f => ↑f i) → b ≤ sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
rintro _ ⟨⟨_, ⟨j, a, ha, rfl⟩, hle⟩, rfl⟩
[GOAL]
case intro.mk.intro.intro.intro.intro
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i j : ι
a : π j
ha : IsAtom a
hle : Function.update ⊥ j a ≤ s
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ j a,
        property :=
          (_ : (∃ i a_1, IsAtom a_1 ∧ Function.update ⊥ j a = Function.update ⊥ i a_1) ∧ Function.update ⊥ j a ≤ s) } ≤
    sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i j : ι
a : π j
ha : IsAtom a
hle : Function.update ⊥ j a ≤ s
hij : i = j
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ j a,
        property :=
          (_ : (∃ i a_1, IsAtom a_1 ∧ Function.update ⊥ j a = Function.update ⊥ i a_1) ∧ Function.update ⊥ j a ≤ s) } ≤
    sSup {a | IsAtom a ∧ a ≤ s i}
case neg
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i j : ι
a : π j
ha : IsAtom a
hle : Function.update ⊥ j a ≤ s
hij : ¬i = j
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ j a,
        property :=
          (_ : (∃ i a_1, IsAtom a_1 ∧ Function.update ⊥ j a = Function.update ⊥ i a_1) ∧ Function.update ⊥ j a ≤ s) } ≤
    sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
case neg => simp [Function.update_noteq hij]
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i j : ι
a : π j
ha : IsAtom a
hle : Function.update ⊥ j a ≤ s
hij : ¬i = j
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ j a,
        property :=
          (_ : (∃ i a_1, IsAtom a_1 ∧ Function.update ⊥ j a = Function.update ⊥ i a_1) ∧ Function.update ⊥ j a ≤ s) } ≤
    sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
case neg => simp [Function.update_noteq hij]
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i j : ι
a : π j
ha : IsAtom a
hle : Function.update ⊥ j a ≤ s
hij : ¬i = j
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ j a,
        property :=
          (_ : (∃ i a_1, IsAtom a_1 ∧ Function.update ⊥ j a = Function.update ⊥ i a_1) ∧ Function.update ⊥ j a ≤ s) } ≤
    sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
simp [Function.update_noteq hij]
[GOAL]
case pos
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i j : ι
a : π j
ha : IsAtom a
hle : Function.update ⊥ j a ≤ s
hij : i = j
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ j a,
        property :=
          (_ : (∃ i a_1, IsAtom a_1 ∧ Function.update ⊥ j a = Function.update ⊥ i a_1) ∧ Function.update ⊥ j a ≤ s) } ≤
    sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
subst hij
[GOAL]
case pos
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
ha : IsAtom a
hle : Function.update ⊥ i a ≤ s
⊢ (fun f => ↑f i)
      { val := Function.update ⊥ i a,
        property :=
          (_ :
            (∃ i_1 a_1, IsAtom a_1 ∧ Function.update ⊥ i a = Function.update ⊥ i_1 a_1) ∧ Function.update ⊥ i a ≤ s) } ≤
    sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
simp only [Function.update_same]
[GOAL]
case pos
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
ha : IsAtom a
hle : Function.update ⊥ i a ≤ s
⊢ a ≤ sSup {a | IsAtom a ∧ a ≤ s i}
[PROOFSTEP]
refine le_sSup ⟨ha, by simpa using hle i⟩
[GOAL]
ι : Type ?u.135698
α : Type u_1
β : Type u_2
π : ι → Type u
inst✝¹ : (i : ι) → CompleteLattice (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
a : π i
ha : IsAtom a
hle : Function.update ⊥ i a ≤ s
⊢ a ≤ s i
[PROOFSTEP]
simpa using hle i
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ IsAtom s ↔ ∃ x, s = {x}
[PROOFSTEP]
refine'
  ⟨_, by
    rintro ⟨x, rfl⟩
    exact isAtom_singleton x⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ (∃ x, s = {x}) → IsAtom s
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
x : α
⊢ IsAtom {x}
[PROOFSTEP]
exact isAtom_singleton x
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ IsAtom s → ∃ x, s = {x}
[PROOFSTEP]
rw [_root_.isAtom_iff, bot_eq_empty, ← nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ (Set.Nonempty s ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ x, s = {x}
[PROOFSTEP]
rintro ⟨⟨x, hx⟩, hs⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}
[PROOFSTEP]
exact
  ⟨x,
    eq_singleton_iff_unique_mem.2
      ⟨hx, fun y hy => (hs { y } (singleton_ne_empty _) (singleton_subset_iff.2 hy) hx).symm⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ IsCoatom s ↔ ∃ x, s = {x}ᶜ
[PROOFSTEP]
rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ
[PROOFSTEP]
simp_rw [@eq_comm _ s, compl_eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ s = sSup ((fun x => {x}) '' s)
[PROOFSTEP]
rw [sSup_eq_sUnion, sUnion_image, biUnion_of_singleton]
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ ∀ (a : Set α), a ∈ (fun x => {x}) '' s → IsAtom a
[PROOFSTEP]
{ rintro _ ⟨x, _, rfl⟩
  exact isAtom_singleton x
}
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ ∀ (a : Set α), a ∈ (fun x => {x}) '' s → IsAtom a
[PROOFSTEP]
rintro _ ⟨x, _, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
x : α
left✝ : x ∈ s
⊢ IsAtom ((fun x => {x}) x)
[PROOFSTEP]
exact isAtom_singleton x
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ s = sInf ((fun x => {x}ᶜ) '' sᶜ)
[PROOFSTEP]
{rw [sInf_eq_sInter, sInter_image, ← compl_iUnion₂, biUnion_of_singleton, compl_compl]
}
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ s = sInf ((fun x => {x}ᶜ) '' sᶜ)
[PROOFSTEP]
rw [sInf_eq_sInter, sInter_image, ← compl_iUnion₂, biUnion_of_singleton, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ ∀ (a : Set α), a ∈ (fun x => {x}ᶜ) '' sᶜ → IsCoatom a
[PROOFSTEP]
{ rintro _ ⟨x, _, rfl⟩
  exact isCoatom_singleton_compl x
}
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
⊢ ∀ (a : Set α), a ∈ (fun x => {x}ᶜ) '' sᶜ → IsCoatom a
[PROOFSTEP]
rintro _ ⟨x, _, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
x : α
left✝ : x ∈ sᶜ
⊢ IsCoatom ((fun x => {x}ᶜ) x)
[PROOFSTEP]
exact isCoatom_singleton_compl x