α : Type u_1
β : Type ?u.512
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      Finset.univ =
    {⊤, ⊥}
α : Type u_1
β : Type ?u.512
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.univ = {⊤, ⊥}
change Finset.map _ (Finset.univ : Finset Bool) = _
α : Type u_1
β : Type ?u.512
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      {true, false} =
    {⊤, ⊥}
α : Type u_1
β : Type ?u.512
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      Finset.univ =
    {⊤, ⊥}
rw [Fintype.univ_bool]
α : Type u_1
β : Type ?u.512
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ {↑IsSimpleOrder.equivBool.symm true, ↑IsSimpleOrder.equivBool.symm false} = {⊤, ⊥}
α : Type u_1
β : Type ?u.512
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      {true, false} =
    {⊤, ⊥}
simp only [Finset.map_insert, Function.Embedding.coeFn_mk, Finset.map_singleton]
no goals
α : Type u_1
β : Type ?u.512
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ {↑IsSimpleOrder.equivBool.symm true, ↑IsSimpleOrder.equivBool.symm false} = {⊤, ⊥}
rfl