-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c
refine_1 : (a_1 : { x : β × α // Prod.Lex s r x (b, a) }) → { x : β // s x b } × α ⊕ { x : α // r x a }
refine_2 :
  ∀ (a_1 b_1 : { x : β × α // Prod.Lex s r x (b, a) }),
    Subrel (Prod.Lex s r) (fun (x : β × α) ↦ Prod.Lex s r x (b, a)) a_1 b_1 →
      Sum.Lex (α := { x : β // s x b } × α) (β := { x : α // r x a }) (Prod.Lex (Subrel s fun (x : β) ↦ s x b) r)
        (Subrel r fun (x : α) ↦ r x a)
        ((fun (a_3 : { x : β × α // Prod.Lex s r x (b, a) }) ↦
            (Subtype.casesOn (p := fun (x : β × α) ↦ Prod.Lex s r x (b, a)) (motive :=
                fun (x : { x : β × α // Prod.Lex s r x (b, a) }) ↦ { x : β // s x b } × α ⊕ { x : α // r x a }) a_3
                fun (val : β × α) (h : Prod.Lex s r val (b, a)) ↦
                Prod.casesOn (motive := fun (x : β × α) ↦
                  (h : Prod.Lex s r x (b, a)) → { x : β // s x b } × α ⊕ { x : α // r x a }) val
                  (fun (b' : β) (a' : α) (h : Prod.Lex s r (b', a') (b, a)) ↦
                    if e : b = b' then Sum.inr (Subtype.mk (p := fun (x : α) ↦ r x a) a' ⋯)
                    else Sum.inl (Subtype.mk (p := fun (x : β) ↦ s x b) b' ⋯, a'))
                  h :
              { x : β // s x b } × α ⊕ { x : α // r x a }))
          a_1)
        ((fun (a_3 : { x : β × α // Prod.Lex s r x (b, a) }) ↦
            (Subtype.casesOn (p := fun (x : β × α) ↦ Prod.Lex s r x (b, a)) (motive :=
                fun (x : { x : β × α // Prod.Lex s r x (b, a) }) ↦ { x : β // s x b } × α ⊕ { x : α // r x a }) a_3
                fun (val : β × α) (h : Prod.Lex s r val (b, a)) ↦
                Prod.casesOn (motive := fun (x : β × α) ↦
                  (h : Prod.Lex s r x (b, a)) → { x : β // s x b } × α ⊕ { x : α // r x a }) val
                  (fun (b' : β) (a' : α) (h : Prod.Lex s r (b', a') (b, a)) ↦
                    if e : b = b' then Sum.inr (Subtype.mk (p := fun (x : α) ↦ r x a) a' ⋯)
                    else Sum.inl (Subtype.mk (p := fun (x : β) ↦ s x b) b' ⋯, a'))
                  h :
              { x : β // s x b } × α ⊕ { x : α // r x a }))
          b_1)
⊢ ((typein (Prod.Lex s r)).toRelEmbedding (r := Prod.Lex s r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) :
        (a : β × α) → Ordinal.{u_4})
      (b, a) <
    c

Tactic:
refine (RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this

Premises used: RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone, LE.le.trans_lt