α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 1 + ω ≤ ω
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 1 + ω = ω
refine' le_antisymm _ (le_add_left _ _)
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ type (Sum.Lex EmptyRelation fun x x_1 => x < x_1) ≤ type fun x x_1 => x < x_1
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 1 + ω ≤ ω
rw [omega, ← lift_one.{_, 0}, ← lift_add, lift_le, ← type_unit, ← type_sum_lex]
case refine'_1
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Unit ⊕ ℕ → ℕ

case refine'_2
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (a b : Unit ⊕ ℕ), Sum.Lex EmptyRelation (fun x x_1 => x < x_1) a b → ?refine'_1 a < ?refine'_1 b
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ type (Sum.Lex EmptyRelation fun x x_1 => x < x_1) ≤ type fun x x_1 => x < x_1
refine' ⟨RelEmbedding.collapse (RelEmbedding.ofMonotone _ _)⟩
case refine'_1.inl
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Unit → ℕ

case refine'_1.inr
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ℕ → ℕ
case refine'_1
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Unit ⊕ ℕ → ℕ
apply Sum.rec
case refine'_1.inr
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ℕ → ℕ
case refine'_1.inl
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Unit → ℕ

case refine'_1.inr
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ℕ → ℕ
exact fun _ => 0
no goals
case refine'_1.inr
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ℕ → ℕ
exact Nat.succ
case refine'_2
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Unit ⊕ ℕ
⊢ Sum.Lex EmptyRelation (fun x x_1 => x < x_1) a b → Sum.rec (fun x => 0) Nat.succ a < Sum.rec (fun x => 0) Nat.succ b
case refine'_2
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (a b : Unit ⊕ ℕ),
    Sum.Lex EmptyRelation (fun x x_1 => x < x_1) a b → Sum.rec (fun x => 0) Nat.succ a < Sum.rec (fun x => 0) Nat.succ b
intro a b
no goals
case refine'_2
α : Type ?u.134018
β : Type ?u.134021
γ : Type ?u.134024
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Unit ⊕ ℕ
⊢ Sum.Lex EmptyRelation (fun x x_1 => x < x_1) a b → Sum.rec (fun x => 0) Nat.succ a < Sum.rec (fun x => 0) Nat.succ b
cases a <;> cases b <;> intro H <;> cases' H with _ _ H _ _ H <;>
  [exact H.elim; exact Nat.succ_pos _; exact Nat.succ_lt_succ H]