simp only [mem_dualAnnihilator, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  dualMap_apply_symm]
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ x ∈ (map e U).dualAnnihilator ↔ x ∈ map e.symm.dualMap U.dualAnnihilator
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∀ a ∈ U, x (e a) = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x