case intro.intro
α : Type u
β : Type v
γ : Type ?u.3585
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
b : β
w : α
h : w ∈ c
h' : ↑f w = b
⊢ b ∈ map c f
α : Type u
β : Type v
γ : Type ?u.3585
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
b : β
h : ∃ a, a ∈ c ∧ ↑f a = b
⊢ b ∈ map c f
rcases h with ⟨w, h, h'⟩
case intro.intro
α : Type u
β : Type v
γ : Type ?u.3585
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
w : α
h : w ∈ c
⊢ ↑f w ∈ map c f
case intro.intro
α : Type u
β : Type v
γ : Type ?u.3585
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
b : β
w : α
h : w ∈ c
h' : ↑f w = b
⊢ b ∈ map c f
subst b
no goals
case intro.intro
α : Type u
β : Type v
γ : Type ?u.3585
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
w : α
h : w ∈ c
⊢ ↑f w ∈ map c f
apply mem_map c _ h