α✝ : Type ?u.73654
β✝ : Type ?u.73657
γ : Type ?u.73660
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
x✝ : ↑{b | r b a}
x : α
h : x ∈ {b | r b a}
⊢ ↑f.toRelEmbedding (↑(Subrel.relEmbedding r {b | r b a}) { val := x, property := h }) ∈ {b | s b (↑f a)}
α✝ : Type ?u.73654
β✝ : Type ?u.73657
γ : Type ?u.73660
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
x✝ : ↑{b | r b a}
x : α
h : x ∈ {b | r b a}
⊢ ↑(RelEmbedding.trans (Subrel.relEmbedding r {b | r b a}) f.toRelEmbedding) { val := x, property := h } ∈
    {b | s b (↑f a)}
rw [RelEmbedding.trans_apply]
no goals
α✝ : Type ?u.73654
β✝ : Type ?u.73657
γ : Type ?u.73660
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
x✝ : ↑{b | r b a}
x : α
h : x ∈ {b | r b a}
⊢ ↑f.toRelEmbedding (↑(Subrel.relEmbedding r {b | r b a}) { val := x, property := h }) ∈ {b | s b (↑f a)}
exact f.toRelEmbedding.map_rel_iff.2 h
case intro
α✝ : Type ?u.73654
β✝ : Type ?u.73657
γ : Type ?u.73660
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a✝ : α
x✝ : ↑{b | s b (↑f a✝)}
a : α
h : ↑f a ∈ {b | s b (↑f a✝)}
⊢ ∃ a_1,
    ↑(RelEmbedding.codRestrict {b | s b (↑f a✝)}
            (RelEmbedding.trans (Subrel.relEmbedding r {b | r b a✝}) f.toRelEmbedding)
            (_ :
              ∀ (x : ↑{b | r b a✝}),
                ↑(RelEmbedding.trans (Subrel.relEmbedding r {b | r b a✝}) f.toRelEmbedding) x ∈ {b | s b (↑f a✝)}))
        a_1 =
      { val := ↑f a, property := h }
α✝ : Type ?u.73654
β✝ : Type ?u.73657
γ : Type ?u.73660
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
x✝ : ↑{b | s b (↑f a)}
y : β
h : y ∈ {b | s b (↑f a)}
⊢ ∃ a_1,
    ↑(RelEmbedding.codRestrict {b | s b (↑f a)}
            (RelEmbedding.trans (Subrel.relEmbedding r {b | r b a}) f.toRelEmbedding)
            (_ :
              ∀ (x : ↑{b | r b a}),
                ↑(RelEmbedding.trans (Subrel.relEmbedding r {b | r b a}) f.toRelEmbedding) x ∈ {b | s b (↑f a)}))
        a_1 =
      { val := y, property := h }
rcases f.init h with ⟨a, rfl⟩
no goals
case intro
α✝ : Type ?u.73654
β✝ : Type ?u.73657
γ : Type ?u.73660
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a✝ : α
x✝ : ↑{b | s b (↑f a✝)}
a : α
h : ↑f a ∈ {b | s b (↑f a✝)}
⊢ ∃ a_1,
    ↑(RelEmbedding.codRestrict {b | s b (↑f a✝)}
            (RelEmbedding.trans (Subrel.relEmbedding r {b | r b a✝}) f.toRelEmbedding)
            (_ :
              ∀ (x : ↑{b | r b a✝}),
                ↑(RelEmbedding.trans (Subrel.relEmbedding r {b | r b a✝}) f.toRelEmbedding) x ∈ {b | s b (↑f a✝)}))
        a_1 =
      { val := ↑f a, property := h }
exact ⟨⟨a, f.toRelEmbedding.map_rel_iff.1 h⟩,
  Subtype.eq <| RelEmbedding.trans_apply _ _ _⟩