Quadratic Twist Var Change map

lemma quadraticTwistVarChange_map {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) :    (E.quadraticTwistVarChange L).map σ.toAlgHom.toRingHom      = (E.quadraticTwistVarChange L) * (E.baseChange L).negVariableChange := by  set σ₀ := (exists_algEquiv_ne_one K L).choose  have hσ₀ : σ₀ ≠ 1 := (exists_algEquiv_ne_one K L).choose_spec  obtain rfl : σ = σ₀ := (algEquiv_eq_one_or_eq K L hσ₀ σ).resolve_left hσ  have hcoc := (E.exists_smul_baseChange_and_map_eq L    (exists_notMem_range_algebraMap K L).choose_spec    (exists_algEquiv_ne_one K L).choose_spec).choose_spec.2  have hinv : ∀ C : VariableChange L,      C⁻¹.map σ₀.toAlgHom.toRingHom = (C.map σ₀.toAlgHom.toRingHom)⁻¹ :=    fun C ↦ map_inv (VariableChange.mapHom _) C  unfold quadraticTwistVarChange  rw [hinv, hcoc, mul_inv_rev, (E.baseChange L).negVariableChange_inv]