α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
⊢ Acc s b → Acc r a
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
⊢ Acc s (↑f a) → Acc r a
generalize h : f a = b
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
ac : Acc s b
⊢ Acc r a
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
⊢ Acc s b → Acc r a
intro ac
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h✝ : ↑f a✝ = b
x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), ↑f a = y → Acc r a
a : α
h : ↑f a = x✝
⊢ Acc r a
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
ac : Acc s b
⊢ Acc r a
induction' ac with _ H IH generalizing a
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h : ↑f a✝ = b
a : α
H : ∀ (y : β), s y (↑f a) → Acc s y
IH : ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r a
⊢ Acc r a
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h✝ : ↑f a✝ = b
x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), ↑f a = y → Acc r a
a : α
h : ↑f a = x✝
⊢ Acc r a
subst h
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.41887
δ : Type ?u.41890
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h : ↑f a✝ = b
a : α
H : ∀ (y : β), s y (↑f a) → Acc s y
IH : ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r a
⊢ Acc r a
exact ⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩