α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ ↑(PEquiv.symm f) b
h₂ : a₂ ∈ ↑(PEquiv.symm f) b
⊢ a₁ = a₂
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : b ∈ ↑f a₁
h₂ : b ∈ ↑f a₂
⊢ a₁ = a₂
rw [← mem_iff_mem] at *
no goals
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ ↑(PEquiv.symm f) b
h₂ : a₂ ∈ ↑(PEquiv.symm f) b
⊢ a₁ = a₂
cases h : f.symm b <;> simp_all