α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
⊢ type r + 1 ≤ type s
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
⊢ type r + 1 ≤ type s
haveI := hs
case refine'_1
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a b : α ⊕ PUnit
⊢ Sum.Lex r EmptyRelation a b →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)

case refine'_2
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α ⊕ PUnit
b : β
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
⊢ type r + 1 ≤ type s
refine' ⟨⟨RelEmbedding.ofMonotone (Sum.rec f fun _ => t) (fun a b ↦ _), fun a b ↦ _⟩⟩
case refine'_1.inl.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a b : α
⊢ Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inl b) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl b))

case refine'_1.inl.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
⊢ Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))

case refine'_1.inr.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
val✝ : PUnit
b : α
⊢ Sum.Lex r EmptyRelation (Sum.inr val✝) (Sum.inl b) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl b))

case refine'_1.inr.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
val✝¹ val✝ : PUnit
⊢ Sum.Lex r EmptyRelation (Sum.inr val✝¹) (Sum.inr val✝) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝¹))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
case refine'_1
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a b : α ⊕ PUnit
⊢ Sum.Lex r EmptyRelation a b →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)
rcases a with (a | _) <;> rcases b with (b | _)
no goals
case refine'_1.inl.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a b : α
⊢ Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inl b) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl b))
simpa only [Sum.lex_inl_inl] using f.map_rel_iff.2
case refine'_1.inl.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝¹ b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
a✝ : Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝)
⊢ s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
case refine'_1.inl.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
⊢ Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
intro
case refine'_1.inl.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝¹ b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
a✝ : Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝)
⊢ ∃ a_1, ↑f a_1 = (fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)
case refine'_1.inl.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝¹ b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
a✝ : Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝)
⊢ s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
rw [hf]
no goals
case refine'_1.inl.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝¹ b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
a✝ : Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝)
⊢ ∃ a_1, ↑f a_1 = (fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)
exact ⟨_, rfl⟩
no goals
case refine'_1.inr.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
val✝ : PUnit
b : α
⊢ Sum.Lex r EmptyRelation (Sum.inr val✝) (Sum.inl b) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl b))
exact False.elim ∘ Sum.lex_inr_inl
no goals
case refine'_1.inr.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
val✝¹ val✝ : PUnit
⊢ Sum.Lex r EmptyRelation (Sum.inr val✝¹) (Sum.inr val✝) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝¹))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
exact False.elim ∘ Sum.lex_inr_inr.1
case refine'_2.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        (Sum.inl a)) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b

case refine'_2.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        (Sum.inr val✝)) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
case refine'_2
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α ⊕ PUnit
b : β
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
rcases a with (a | _)
case refine'_2.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
case refine'_2.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        (Sum.inl a)) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
intro h
case refine'_2.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this✝ : IsWellOrder β s
b : β
a : α
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
this : ∃ a', ↑{ toRelEmbedding := f, top := t, down' := hf }.toRelEmbedding a' = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
case refine'_2.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
have := @PrincipalSeg.init _ _ _ _ _ ⟨f, t, hf⟩ _ _ h
case refine'_2.inl.intro
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
h✝ :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
w : α
h : ↑{ toRelEmbedding := f, top := t, down' := hf }.toRelEmbedding w = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
case refine'_2.inl
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this✝ : IsWellOrder β s
b : β
a : α
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
this : ∃ a', ↑{ toRelEmbedding := f, top := t, down' := hf }.toRelEmbedding a' = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
cases' this with w h
no goals
case refine'_2.inl.intro
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
h✝ :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
w : α
h : ↑{ toRelEmbedding := f, top := t, down' := hf }.toRelEmbedding w = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
exact ⟨Sum.inl w, h⟩
case refine'_2.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inr val✝))
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
case refine'_2.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        (Sum.inr val✝)) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
intro h
case refine'_2.inr.intro
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
h✝ :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inr val✝))
w : α
h : ↑f w = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
case refine'_2.inr
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inr val✝))
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
cases' (hf b).1 h with w h
no goals
case refine'_2.inr.intro
α✝ : Type ?u.168588
β✝ : Type ?u.168591
γ : Type ?u.168594
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal
α : Type u_1
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_1
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
h✝ :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inr val✝))
w : α
h : ↑f w = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
exact ⟨Sum.inl w, h⟩