no goals
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Bijective ↑(dualMap f) ↔ Function.Bijective ↑f
simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]