Quadratic Twist Var Change base Change map

lemma quadraticTwistVarChange_baseChange_map {σ : M ≃ₐ[K] M}    (hσ : ¬ ∀ x : L, σ (algebraMap L M x) = algebraMap L M x) :    ((E.quadraticTwistVarChange L).baseChange M).map σ.toAlgHom.toRingHom      = (E.quadraticTwistVarChange L).baseChange M * (E.baseChange M).negVariableChange := by  obtain ⟨σ₀, hσ₀⟩ := exists_algEquiv_ne_one K L  have hres : σ.restrictNormal L = σ₀ :=    (algEquiv_eq_one_or_eq K L hσ₀ _).resolve_left      (fun h ↦ hσ ((forall_apply_algebraMap_iff_restrictNormal_eq_one K L M σ).mpr h))  have hcomp : σ.toAlgHom.toRingHom.comp (algebraMap L M)      = (algebraMap L M).comp σ₀.toAlgHom.toRingHom := by    ext l    have h := (AlgEquiv.restrictNormal_commutes σ L l).symm    rw [hres] at h    simpa using h  have e1 : ((E.quadraticTwistVarChange L).baseChange M).map σ.toAlgHom.toRingHom      = (E.quadraticTwistVarChange L).map (σ.toAlgHom.toRingHom.comp (algebraMap L M)) :=    (E.quadraticTwistVarChange L).map_map (algebraMap L M) σ.toAlgHom.toRingHom  have e2 : ((E.quadraticTwistVarChange L) * (E.baseChange L).negVariableChange).map        (algebraMap L M)      = (E.quadraticTwistVarChange L).baseChange M        * (E.baseChange L).negVariableChange.map (algebraMap L M) :=    map_mul (VariableChange.mapHom (algebraMap L M)) _ _  rw [e1, hcomp, ← VariableChange.map_map, E.quadraticTwistVarChange_map L hσ₀, e2,    negVariableChange_map, baseChange_map_algebraMap]