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