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