-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_le_of_limit_aux {α β r s} [IsWellOrder α r] [IsWellOrder β s] {c}
    (h : IsLimit (type s)) (H : ∀ b' < type s, type r * b' ≤ c) (l : c < type r * type s) :
    False

Proof state:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

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

Result:
case refine_1
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a✝ < c
a : { x // Prod.Lex s r x (b, a✝) }
⊢ { x // s x b } × α ⊕ { x // r x a✝ }

case refine_2
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b✝ : β
this✝ : type r * (typein s).toRelEmbedding b✝ + type r ≤ c
this : type r * (typein s).toRelEmbedding b✝ + (typein r).toRelEmbedding a✝ < c
a b : { x // Prod.Lex s r x (b✝, a✝) }
⊢ Subrel (Prod.Lex s r) (fun x => Prod.Lex s r x (b✝, a✝)) a b →
    Sum.Lex (Prod.Lex (Subrel s fun x => s x b✝) r) (Subrel r fun x => r x a✝) ((fun a => ?refine_1) a)
      ((fun a => ?refine_1) b)

Proof state:
case neg.right
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
a' : α
e : ¬b = b
h : r a' a
⊢ s b b

Tactic:
exact (e rfl).elim

Result:
no goals

Proof state:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this : type r * (typein s).toRelEmbedding b + type r ≤ c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

Tactic:
have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this

Result:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

Proof state:
case neg
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
a₁ : α
b₂ : β
a₂ : α
h₂ : Prod.Lex s r (b₂, a₂) (b, a)
e₂ : ¬b = b₂
h₁ : Prod.Lex s r (b, a₁) (b, a)
h : s b b₂
⊢ False

Tactic:
obtain ⟨-, -, h₂_h⟩ | e₂ := h₂ <;> [exact asymm h h₂_h; exact e₂ rfl]

Result:
no goals

Proof state:
case neg
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
a₁ : α
b₂ : β
a₂ : α
h₂ : Prod.Lex s r (b₂, a₂) (b, a)
e₂ : ¬b = b₂
h₁ : Prod.Lex s r (b, a₁) (b, a)
h : Subrel (Prod.Lex s r) (fun x => Prod.Lex s r x (b, a)) ⟨(b, a₁), h₁⟩ ⟨(b₂, a₂), h₂⟩
⊢ Sum.Lex (Prod.Lex (Subrel s fun x => s x b) r) (Subrel r fun x => r x a)
    ((fun a_1 =>
        Subtype.casesOn a_1 fun val h =>
          Prod.casesOn (motive := fun x => Prod.Lex s r x (b, a) → { x // s x b } × α ⊕ { x // r x a }) val
            (fun b' a' h => if e : b = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)
      ⟨(b, a₁), h₁⟩)
    ((fun a_1 =>
        Subtype.casesOn a_1 fun val h =>
          Prod.casesOn (motive := fun x => Prod.Lex s r x (b, a) → { x // s x b } × α ⊕ { x // r x a }) val
            (fun b' a' h => if e : b = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)
      ⟨(b₂, a₂), h₂⟩)

Tactic:
simp only [subrel_val, Prod.lex_def, e₂, Prod.lex_def, dif_pos, subrel_val, eq_self_iff_true,
  or_false, dif_neg, not_false_iff, Sum.lex_inr_inl, false_and] at h ⊢

Result:
case neg
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
a₁ : α
b₂ : β
a₂ : α
h₂ : Prod.Lex s r (b₂, a₂) (b, a)
e₂ : ¬b = b₂
h₁ : Prod.Lex s r (b, a₁) (b, a)
h : s b b₂
⊢ False

Proof state:
case pos
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
a₁ a₂ : α
h₁ : Prod.Lex s r (b, a₁) (b, a)
h₂ : Prod.Lex s r (b, a₂) (b, a)
h : Subrel (Prod.Lex s r) (fun x => Prod.Lex s r x (b, a)) ⟨(b, a₁), h₁⟩ ⟨(b, a₂), h₂⟩
⊢ Sum.Lex (Prod.Lex (Subrel s fun x => s x b) r) (Subrel r fun x => r x a)
    ((fun a_1 =>
        Subtype.casesOn a_1 fun val h =>
          Prod.casesOn (motive := fun x => Prod.Lex s r x (b, a) → { x // s x b } × α ⊕ { x // r x a }) val
            (fun b' a' h => if e : b = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)
      ⟨(b, a₁), h₁⟩)
    ((fun a_1 =>
        Subtype.casesOn a_1 fun val h =>
          Prod.casesOn (motive := fun x => Prod.Lex s r x (b, a) → { x // s x b } × α ⊕ { x // r x a }) val
            (fun b' a' h => if e : b = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)
      ⟨(b, a₂), h₂⟩)

Tactic:
simpa only [subrel_val, Prod.lex_def, @irrefl _ s _ b, true_and, false_or,
  eq_self_iff_true, dif_pos, Sum.lex_inr_inr] using h

Result:
no goals

Proof state:
case neg.left
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
b : β
this : type r * (typein s).toRelEmbedding b + type r ≤ c
b' : β
e : ¬b = b'
h : s b' b
⊢ s b' b

Tactic:
exact h

Result:
no goals

Proof state:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
this : ∀ (a : α) (b : β), Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)
⊢ False

Tactic:
obtain ⟨b, a⟩ := enum _ ⟨_, l⟩

Result:
case mk
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
this : ∀ (a : α) (b : β), Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)
b : β
a : α
⊢ False