Injective update iff

@[simp]theorem injective_update_iff (p : DualPair E) {φ : E →L[ℝ] F} (hφ : Injective φ) {w : F} :    Injective (p.update φ w) ↔ w ∉ (p.π.ker).map (φ : E →ₛₗ[.id ℝ] F) := by  constructor  · rintro h ⟨u, hu, rfl⟩    have : p.update φ (φ u) p.v = φ u := p.update_v φ (φ u)    nth_rw 2 [← p.update_ker_pi φ (φ u) hu] at this    simp [← h this, p.pairing] at hu  · intro hw    refine (injective_iff_map_eq_zero (p.update φ w)).mpr fun x hx ↦ ?_    rcases p.decomp x with ⟨u, hu, t, rfl⟩    rw [map_add, map_smul, update_v, p.update_ker_pi _ _ hu] at hx    obtain rfl : t = 0 := by      by_contra ht      apply hw      refine ⟨-t⁻¹ • u, (p.π.ker).smul_mem _ hu, ?_⟩      rw [map_smul]      have : -t⁻¹ • (φ u + t • w) + w = -t⁻¹ • (0 : F) + w := congr_arg (-t⁻¹ • · + w) hx      rwa [smul_add, neg_smul, neg_smul, inv_smul_smul₀ ht, smul_zero, zero_add,        neg_add_cancel_right, ← neg_smul] at this    rw [zero_smul, add_zero] at hx ⊢    exact (injective_iff_map_eq_zero φ).mp hφ u hx