-- 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:
case refine_2.mk.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
a : α
b✝ : β
this✝ : type r * (typein s).toRelEmbedding b✝ + type r ≤ c
this : type r * (typein s).toRelEmbedding b✝ + (typein r).toRelEmbedding a < c
b : { x // Prod.Lex s r x (b✝, a) }
b₁ : β
a₁ : α
h₁ : Prod.Lex s r (b₁, a₁) (b✝, a)
⊢ Subrel (Prod.Lex s r) (fun x => Prod.Lex s r x (b✝, a)) ⟨(b₁, a₁), h₁⟩ b →
    Sum.Lex (Prod.Lex (Subrel s fun x => s x b✝) r) (Subrel r fun x => r x a)
      ((fun a_2 =>
          Subtype.casesOn a_2 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_2 =>
          Subtype.casesOn a_2 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)

Tactic:
rcases b with ⟨⟨b₂, a₂⟩, h₂⟩

Result:
case refine_2.mk.mk.mk.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
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b₁ : β
a₁ : α
h₁ : Prod.Lex s r (b₁, a₁) (b, a)
b₂ : β
a₂ : α
h₂ : Prod.Lex s r (b₂, a₂) (b, a)
⊢ 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_2 =>
          Subtype.casesOn a_2 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_2 =>
          Subtype.casesOn a_2 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₂⟩)

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
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ r a' a

Tactic:
subst e

Result:
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' : α
h : Prod.Lex s r (b, a') (b, a)
⊢ r a' a

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 : β), Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)

Tactic:
intro a b

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 : β
⊢ Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)

Proof state:
case pos.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
a : α
b : β
this : type r * (typein s).toRelEmbedding b + type r ≤ c
a' : α
h : s b b
⊢ r a' a

Tactic:
exact (irrefl _ h).elim

Result:
no goals

Proof state:
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

Tactic:
exact irrefl _ (this _ _)

Result:
no goals

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
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ { x // s x b } × α ⊕ { x // r x a }

Tactic:
refine Sum.inr ⟨a', ?_⟩

Result:
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
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ r a' a