case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ ↑(PEquiv.trans f (PEquiv.symm f)) x✝ ↔ a✝ ∈ ↑(ofSet {a | isSome (↑f a) = true}) x✝
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans f (PEquiv.symm f) = ofSet {a | isSome (↑f a) = true}
ext
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ Option.bind (↑f x✝) ↑(PEquiv.symm f) ↔ a✝ ∈ ↑(ofSet {a | isSome (↑f a) = true}) x✝
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ ↑(PEquiv.trans f (PEquiv.symm f)) x✝ ↔ a✝ ∈ ↑(ofSet {a | isSome (↑f a) = true}) x✝
dsimp [PEquiv.trans]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a) ↔ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ Option.bind (↑f x✝) ↑(PEquiv.symm f) ↔ a✝ ∈ ↑(ofSet {a | isSome (↑f a) = true}) x✝
simp only [eq_some_iff f, Option.isSome_iff_exists, Option.mem_def, bind_eq_some',
  ofSet_eq_some_iff]
case h.a.mp
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a) → a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}

case h.a.mpr
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1} → ∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a) ↔ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
constructor
case h.a.mp.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
b : β
hb₁ : ↑f x✝ = some b
hb₂ : ↑f a✝ = some b
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
case h.a.mp
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a) → a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
rintro ⟨b, hb₁, hb₂⟩
no goals
case h.a.mp.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
b : β
hb₁ : ↑f x✝ = some b
hb₂ : ↑f a✝ = some b
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
exact ⟨PEquiv.inj _ hb₂ hb₁, b, hb₂⟩
no goals
case h.a.mpr
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1} → ∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a
simp (config := { contextual := true })