-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
a b : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
x : Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)
ao : Γ
ac : FiniteArchimedeanClass R
x_1 : Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)
bo : Γ
bc : FiniteArchimedeanClass R
h :
  LE.le (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (bo, bc) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
inl :
  ∀
    (h :
      LT.lt.{u_1} (α := Γ)
        ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac))).1
        ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (bo, bc))).1),
    LE.le (α := FiniteArchimedeanClass (Lex R⟦Γ⟧))
      ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
          ((FiniteArchimedeanClass.liftOrderHom
                  (fun (a : { a : R // a ≠ 0 }) ↦
                    FiniteArchimedeanClass.mk
                      ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                        ((single
                              ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                            (a : R) → R⟦Γ⟧)
                          (↑a : R)))
                      ⋯)
                  ⋯ :
                (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
              ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
            FiniteArchimedeanClass (Lex R⟦Γ⟧)))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac)))
      ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
          ((FiniteArchimedeanClass.liftOrderHom
                  (fun (a : { a : R // a ≠ 0 }) ↦
                    FiniteArchimedeanClass.mk
                      ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                        ((single
                              ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                            (a : R) → R⟦Γ⟧)
                          (↑a : R)))
                      ⋯)
                  ⋯ :
                (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
              ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
            FiniteArchimedeanClass (Lex R⟦Γ⟧)))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (bo, bc)))
⊢ LE.le (α := FiniteArchimedeanClass (Lex R⟦Γ⟧))
    ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
        ((FiniteArchimedeanClass.liftOrderHom
                (fun (a : { a : R // a ≠ 0 }) ↦
                  FiniteArchimedeanClass.mk
                    ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                      ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                          (a : R) → R⟦Γ⟧)
                        (↑a : R)))
                    ⋯)
                ⋯ :
              (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
            ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
          FiniteArchimedeanClass (Lex R⟦Γ⟧)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac)))
    ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
        ((FiniteArchimedeanClass.liftOrderHom
                (fun (a : { a : R // a ≠ 0 }) ↦
                  FiniteArchimedeanClass.mk
                    ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                      ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                          (a : R) → R⟦Γ⟧)
                        (↑a : R)))
                    ⋯)
                ⋯ :
              (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
            ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
          FiniteArchimedeanClass (Lex R⟦Γ⟧)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (bo, bc)))
have inr : ∀
  (h :
    LE.le (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac) :
        Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
          (((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
                ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac))).1,
            bc) :
        Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))))
  (hle :
    LE.le.{u_2} (α := FiniteArchimedeanClass R)
      ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
          ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac))).2
      ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
          ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
            (((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
                  ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac))).1,
              bc))).2),
  LE.le (α := FiniteArchimedeanClass (Lex R⟦Γ⟧))
    ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
        ((FiniteArchimedeanClass.liftOrderHom
                (fun (a : { a : R // a ≠ 0 }) ↦
                  FiniteArchimedeanClass.mk
                    ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                      ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                          (a : R) → R⟦Γ⟧)
                        (↑a : R)))
                    sorry)
                sorry :
              (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
            ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
          FiniteArchimedeanClass (Lex R⟦Γ⟧)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac)))
    ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
        ((FiniteArchimedeanClass.liftOrderHom
                (fun (a : { a : R // a ≠ 0 }) ↦
                  FiniteArchimedeanClass.mk
                    ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                      ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                          (a : R) → R⟦Γ⟧)
                        (↑a : R)))
                    sorry)
                sorry :
              (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
            ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
          FiniteArchimedeanClass (Lex R⟦Γ⟧)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
        (((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
              ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (ao, ac))).1,
          bc)))
Tactic: obtain h | ⟨rfl, hle⟩ := Prod.Lex.le_iff.mp h
Cleared hypotheses: bo, h