case intro
α : Type u_1
β : Type u_2
γ : Type ?u.12477
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a a' : α
h : s (↑f a') (↑f a)
⊢ ∃ a'_1, ↑f a'_1 = ↑f a' ∧ r a'_1 a
α : Type u_1
β : Type u_2
γ : Type ?u.12477
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a : α
b : β
h : s b (↑f a)
⊢ ∃ a', ↑f a' = b ∧ r a' a
rcases f.init h with ⟨a', rfl⟩
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.12477
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a a' : α
h : s (↑f a') (↑f a)
⊢ ∃ a'_1, ↑f a'_1 = ↑f a' ∧ r a'_1 a
exact ⟨a', rfl, f.map_rel_iff.1 h⟩