[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.univ = {⊤, ⊥}
[PROOFSTEP]
change Finset.map _ (Finset.univ : Finset Bool) = _
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      Finset.univ =
    {⊤, ⊥}
[PROOFSTEP]
rw [Fintype.univ_bool]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      {true, false} =
    {⊤, ⊥}
[PROOFSTEP]
simp only [Finset.map_insert, Function.Embedding.coeFn_mk, Finset.map_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ {↑IsSimpleOrder.equivBool.symm true, ↑IsSimpleOrder.equivBool.symm false} = {⊤, ⊥}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
a : Bool
⊢ a = ⊥ ∨ a = ⊤
[PROOFSTEP]
rw [← Finset.mem_singleton, Or.comm, ← Finset.mem_insert, top_eq_true, bot_eq_false, ← Fintype.univ_bool]
[GOAL]
α : Type u_1
β : Type u_2
a : Bool
⊢ a ∈ Finset.univ
[PROOFSTEP]
apply Finset.mem_univ
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
⊢ IsCoatomic α
[PROOFSTEP]
refine' IsCoatomic.mk fun b => or_iff_not_imp_left.2 fun ht => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
⊢ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
obtain ⟨c, hc, hmax⟩ := Set.Finite.exists_maximal_wrt id {x : α | b ≤ x ∧ x ≠ ⊤} (Set.toFinite _) ⟨b, le_rfl, ht⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
⊢ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
refine' ⟨c, ⟨hc.2, fun y hcy => _⟩, hc.1⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
y : α
hcy : c < y
⊢ y = ⊤
[PROOFSTEP]
by_contra hyt
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
y : α
hcy : c < y
hyt : ¬y = ⊤
⊢ False
[PROOFSTEP]
obtain rfl : c = y := hmax y ⟨hc.1.trans hcy.le, hyt⟩ hcy.le
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
hcy : c < c
hyt : ¬c = ⊤
⊢ False
[PROOFSTEP]
exact (lt_self_iff_false _).mp hcy
