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
              (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

Tactic:
grind [EmbeddingLike.apply_eq_iff_eq, ofLex_toLex]

Goal state after: