-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_le_of_limit {a b c : Ordinal} (h : IsLimit b) :
    a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c :=
  ⟨fun h _ l => (add_le_add_left l.le _).trans h, fun H =>
    le_of_not_lt <| by
      -- Porting note: `induction` tactics are required because of the parser bug.
      induction a using inductionOn with
      | H α r =>
        induction b using inductionOn with
        | H β s =>
          intro l
          suffices ∀ x : β, Sum.Lex r s (Sum.inr x) (enum _ ⟨_, l⟩) by
            -- Porting note: `revert` & `intro` is required because `cases'` doesn't replace
            --               `enum _ _ l` in `this`.
            revert this; rcases enum _ ⟨_, l⟩ with x | x <;> intro this
            · cases this (enum s ⟨0, h.pos⟩)
            · exact irrefl _ (this _)
          intro x
          rw [← typein_lt_typein (Sum.Lex r s), typein_enum]
          have := H _ (h.succ_lt (typein_lt_type s x))
          rw [add_succ, succ_le_iff] at this
          refine
            (RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this
          · rcases a with ⟨a | b, h⟩
            · exact Sum.inl a
            · exact Sum.inr ⟨b, by cases h; assumption⟩
          · rcases a with ⟨a | a, h₁⟩ <;> rcases b with ⟨b | b, h₂⟩ <;> cases h₁ <;> cases h₂ <;>
              rintro ⟨⟩ <;> constructor <;> assumption⟩

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

Tactic:
rcases a with ⟨a | a, h₁⟩ <;> rcases b with ⟨b | b, h₂⟩ <;> cases h₁ <;> cases h₂ <;>
  rintro ⟨⟩ <;> constructor <;> assumption

Result:
no goals

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

Tactic:
have := H _ (h.succ_lt (typein_lt_type s x))

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

Proof state:
case H.H.refine_1.mk.inl
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h✝ : (type s).IsLimit
H : ∀ b' < type s, type r + b' ≤ c
l : c < type r + type s
x : β
this : type r + (typein s).toRelEmbedding x < c
a : α
h : Sum.Lex r s (Sum.inl a) (Sum.inr x)
⊢ α ⊕ { x_1 // s x_1 x }

Tactic:
exact Sum.inl a

Result:
no goals

Proof state:
case inr
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : (type s).IsLimit
H : ∀ b' < type s, type r + b' ≤ c
l : c < type r + type s
x : β
this : ∀ (x_1 : β), Sum.Lex r s (Sum.inr x_1) (Sum.inr x)
⊢ False

Tactic:
exact irrefl _ (this _)

Result:
no goals

Proof state:
case H.H
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : (type s).IsLimit
H : ∀ b' < type s, type r + b' ≤ c
l : c < type r + type s
⊢ ∀ (x : β), Sum.Lex r s (Sum.inr x) ((enum (Sum.Lex r s)) ⟨c, l⟩)

Tactic:
intro x

Result:
case H.H
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : (type s).IsLimit
H : ∀ b' < type s, type r + b' ≤ c
l : c < type r + type s
x : β
⊢ Sum.Lex r s (Sum.inr x) ((enum (Sum.Lex r s)) ⟨c, l⟩)

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

Tactic:
rw [add_succ, succ_le_iff] at this

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

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

Tactic:
revert this

Result:
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : (type s).IsLimit
H : ∀ b' < type s, type r + b' ≤ c
l : c < type r + type s
⊢ (∀ (x : β), Sum.Lex r s (Sum.inr x) ((enum (Sum.Lex r s)) ⟨c, l⟩)) → False