case intro
α✝ : Type ?u.72894
β✝ : Type ?u.72897
γ : Type ?u.72900
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i s
x✝ : ↑{b | s b f.top}
b : α
h : ↑f.toRelEmbedding b ∈ {b | s b f.top}
⊢ ∃ a,
    ↑(RelEmbedding.codRestrict {b | s b f.top}
            { toRelEmbedding := f.toRelEmbedding,
                init' :=
                  (_ :
                    ∀ (x : α) (x_1 : β),
                      s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) }.toRelEmbedding
            (_ : ∀ (a : α), s (↑f.toRelEmbedding a) f.top))
        a =
      { val := ↑f.toRelEmbedding b, property := h }
α✝ : Type ?u.72894
β✝ : Type ?u.72897
γ : Type ?u.72900
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i s
x✝ : ↑{b | s b f.top}
a : β
h : a ∈ {b | s b f.top}
⊢ ∃ a_1,
    ↑(RelEmbedding.codRestrict {b | s b f.top}
            { toRelEmbedding := f.toRelEmbedding,
                init' :=
                  (_ :
                    ∀ (x : α) (x_1 : β),
                      s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) }.toRelEmbedding
            (_ : ∀ (a : α), s (↑f.toRelEmbedding a) f.top))
        a_1 =
      { val := a, property := h }
rcases f.down.1 h with ⟨b, rfl⟩
no goals
case intro
α✝ : Type ?u.72894
β✝ : Type ?u.72897
γ : Type ?u.72900
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i s
x✝ : ↑{b | s b f.top}
b : α
h : ↑f.toRelEmbedding b ∈ {b | s b f.top}
⊢ ∃ a,
    ↑(RelEmbedding.codRestrict {b | s b f.top}
            { toRelEmbedding := f.toRelEmbedding,
                init' :=
                  (_ :
                    ∀ (x : α) (x_1 : β),
                      s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) }.toRelEmbedding
            (_ : ∀ (a : α), s (↑f.toRelEmbedding a) f.top))
        a =
      { val := ↑f.toRelEmbedding b, property := h }
exact ⟨b, rfl⟩