Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ ∀ {a b : Lex (Lex (α × β) × γ)},
    (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          a ≤
        (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          b ↔
      a ≤ b

Tactic:
simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
      Equiv.prodAssoc_apply]

Goal state after:
α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ ∀ {a b : Lex (Lex (α × β) × γ)},
    (ofLex
              (toLex
                (map ⇑(Equiv.refl α) ⇑toLex
                  ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1, (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                    (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).1 <
          (ofLex
              (toLex
                (map ⇑(Equiv.refl α) ⇑toLex
                  ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1, (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                    (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).1 ∨
        (ofLex
                (toLex
                  (map ⇑(Equiv.refl α) ⇑toLex
                    ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1, (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                      (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).1 =
            (ofLex
                (toLex
                  (map ⇑(Equiv.refl α) ⇑toLex
                    ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1, (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                      (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).1 ∧
          ((ofLex
                  (ofLex
                      (toLex
                        (map ⇑(Equiv.refl α) ⇑toLex
                          ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                            (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                            (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).2).1 <
              (ofLex
                  (ofLex
                      (toLex
                        (map ⇑(Equiv.refl α) ⇑toLex
                          ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                            (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                            (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).2).1 ∨
            (ofLex
                    (ofLex
                        (toLex
                          (map ⇑(Equiv.refl α) ⇑toLex
                            ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).2).1 =
                (ofLex
                    (ofLex
                        (toLex
                          (map ⇑(Equiv.refl α) ⇑toLex
                            ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).2).1 ∧
              (ofLex
                    (ofLex
                        (toLex
                          (map ⇑(Equiv.refl α) ⇑toLex
                            ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).2).2 ≤
                (ofLex
                    (ofLex
                        (toLex
                          (map ⇑(Equiv.refl α) ⇑toLex
                            ((map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                              (map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).2).2) ↔
      ((ofLex (ofLex a).1).1 < (ofLex (ofLex b).1).1 ∨
          (ofLex (ofLex a).1).1 = (ofLex (ofLex b).1).1 ∧ (ofLex (ofLex a).1).2 < (ofLex (ofLex b).1).2) ∨
        (ofLex a).1 = (ofLex b).1 ∧ (ofLex a).2 ≤ (ofLex b).2