-- 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 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 : type r + (typein s).toRelEmbedding x < c
b : β
h✝ : s b x
⊢ s b x

Tactic:
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 : β
⊢ Sum.Lex r s (Sum.inr x) ((enum (Sum.Lex r s)) ⟨c, l⟩)

Tactic:
rw [← typein_lt_typein (Sum.Lex r s), typein_enum]

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 : β
⊢ (typein (Sum.Lex r s)).toRelEmbedding (Sum.inr x) < c

Proof state:
case 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 : ∀ (x_1 : β), Sum.Lex r s (Sum.inr x_1) (Sum.inl x)
⊢ False

Tactic:
cases this (enum s ⟨0, h.pos⟩)

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 : β
this : type r + (typein s).toRelEmbedding x < c
⊢ (typein (Sum.Lex r s)).toRelEmbedding (Sum.inr x) < c

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

Result:
case H.H.refine_1
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 : { x_1 // Sum.Lex r s x_1 (Sum.inr x) }
⊢ α ⊕ { x_1 // s x_1 x }

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 => ?H.H.refine_1) a) ((fun a => ?H.H.refine_1) b)

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
x : β
this : type r + (typein s).toRelEmbedding x < c
b : β
h : Sum.Lex r s (Sum.inr b) (Sum.inr x)
⊢ s b x

Tactic:
cases h

Result:
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 : type r + (typein s).toRelEmbedding x < c
b : β
h✝ : s b x
⊢ s b x

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
⊢ ¬c < type r + type s

Tactic:
intro l

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
⊢ False

Proof state:
case H.H.refine_1.mk.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 : type r + (typein s).toRelEmbedding x < c
b : β
h : Sum.Lex r s (Sum.inr b) (Sum.inr x)
⊢ α ⊕ { x_1 // s x_1 x }

Tactic:
exact Sum.inr ⟨b, by cases h; assumption⟩

Result:
no goals

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
⊢ (∀ (x : β), Sum.Lex r s (Sum.inr x) ((enum (Sum.Lex r s)) ⟨c, l⟩)) → False

Tactic:
rcases enum _ ⟨_, l⟩ with x | x <;> intro this

Result:
case 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 : ∀ (x_1 : β), Sum.Lex r s (Sum.inr x_1) (Sum.inl x)
⊢ False

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

Proof state:
case H.H.refine_1
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 : { x_1 // Sum.Lex r s x_1 (Sum.inr x) }
⊢ α ⊕ { x_1 // s x_1 x }

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

Result:
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 }

case H.H.refine_1.mk.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 : type r + (typein s).toRelEmbedding x < c
b : β
h : Sum.Lex r s (Sum.inr b) (Sum.inr x)
⊢ α ⊕ { x_1 // s x_1 x }