α : Type u_1
β : Type u_2
γ : Type ?u.24005
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (↑f y)
b : β
hb : s b (↑f a)
⊢ Acc s b
α : Type u_1
β : Type u_2
γ : Type ?u.24005
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a : α
⊢ Acc r a → Acc s (↑f a)
refine' fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => _
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.24005
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (↑f y)
a' : α
hb : s (↑f a') (↑f a)
⊢ Acc s (↑f a')
α : Type u_1
β : Type u_2
γ : Type ?u.24005
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (↑f y)
b : β
hb : s b (↑f a)
⊢ Acc s b
obtain ⟨a', rfl⟩ := f.init hb
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.24005
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (↑f y)
a' : α
hb : s (↑f a') (↑f a)
⊢ Acc s (↑f a')
exact ha _ (f.map_rel_iff.mp hb)