no goals
f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (↑e₁ x) = pure (↑e₂ x)
simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x)