[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
src✝ : αᵒᵈ ≃ α := ofDual
⊢ ∀ {a b : αᵒᵈ},
    Adj (hasse α)
        (↑{ 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) ↔
      Adj (hasse αᵒᵈ) a b
[PROOFSTEP]
simp [or_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
⊢ hasse (α × β) = hasse α □ hasse β
[PROOFSTEP]
ext x y
[GOAL]
case Adj.h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ Adj (hasse (α × β)) x y ↔ Adj (hasse α □ hasse β) x y
[PROOFSTEP]
simp_rw [boxProd_adj, hasse_adj, Prod.covby_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2, or_or_or_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ Reachable (hasse α) a b
[PROOFSTEP]
rw [reachable_iff_reflTransGen]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b
[PROOFSTEP]
exact
  reflTransGen_of_succ _ (fun c hc => Or.inl <| covby_succ_of_not_isMax hc.2.not_isMax) fun c hc =>
    Or.inr <| covby_succ_of_not_isMax hc.2.not_isMax
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ Reachable (hasse α) a b
[PROOFSTEP]
rw [reachable_iff_reflTransGen, ← reflTransGen_swap]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (hasse α).Adj) b a
[PROOFSTEP]
exact
  reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covby_of_not_isMin hc.1.not_isMin) fun c hc =>
    Or.inr <| pred_covby_of_not_isMin hc.1.not_isMin
