case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ ↑(PEquiv.trans f (PEquiv.refl β)) x✝ ↔ a✝ ∈ ↑f x✝
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans f (PEquiv.refl β) = f
ext
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ Option.bind (↑f x✝) ↑(PEquiv.refl β) ↔ a✝ ∈ ↑f x✝
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ ↑(PEquiv.trans f (PEquiv.refl β)) x✝ ↔ a✝ ∈ ↑f x✝
dsimp [PEquiv.trans]
no goals
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ Option.bind (↑f x✝) ↑(PEquiv.refl β) ↔ a✝ ∈ ↑f x✝
simp