-- 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
x y : Lex R⟦Γ⟧
mp :
  (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))) ∧
      (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))) →
    Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
      Eq.{u_2 + 1} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
⊢ (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))) ∧
      (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))) ↔
    Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
      Eq.{u_2 + 1} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
have mpr : Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
      (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
    Eq.{u_2 + 1} (α := ArchimedeanClass R)
      (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
      (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))) →
  (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∨
      Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
        LE.le.{u_2} (α := ArchimedeanClass R)
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))) ∧
    (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∨
      Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
        LE.le.{u_2} (α := ArchimedeanClass R)
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))))
Tactic: constructor