no goals
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
classical
  obtain ⟨z, hz⟩ := D.finset_le (Finset.image g Finset.univ)
  exact ⟨z, fun i => hz (g i) (Finset.mem_image_of_mem g (Finset.mem_univ i))⟩
case intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
z : γ
hz : ∀ (i : γ), i ∈ image g univ → r (f i) (f z)
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
obtain ⟨z, hz⟩ := D.finset_le (Finset.image g Finset.univ)
no goals
case intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
z : γ
hz : ∀ (i : γ), i ∈ image g univ → r (f i) (f z)
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
exact ⟨z, fun i => hz (g i) (Finset.mem_image_of_mem g (Finset.mem_univ i))⟩