Exists smul base Change and map eq

theorem exists_smul_baseChange_and_map_eq {θ : L} (hθ : θ ∉ Set.range (algebraMap K L))    {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) :    ∃ C : VariableChange L, C • (E.quadraticTwistBy θ).baseChange L = E.baseChange L ∧      C.map σ.toAlgHom.toRingHom = (E.baseChange L).negVariableChange * C := by  have hσθ : σ θ ≠ θ := algEquiv_apply_ne K L hσ hθ  have hw : σ θ - θ ≠ 0 := sub_ne_zero.mpr hσθ  have hT : algebraMap K L (Algebra.trace K L θ) = θ + σ θ :=    algebraMap_trace_eq_add K L hσ θ  have hN : algebraMap K L (Algebra.norm K θ) = θ * σ θ :=    algebraMap_norm_eq_mul K L hσ θ  have hσσ : σ (σ θ) = θ := by    rw [← AlgEquiv.mul_apply, algEquiv_mul_self K L hσ,      AlgEquiv.one_apply]  have hap : ⇑σ.toAlgHom.toRingHom = ⇑σ := rfl  refine ⟨⟨Units.mk0 (σ θ - θ) hw, 0, -(θ * algebraMap K L E.a₁),    -((σ θ - θ) ^ 2 * θ * algebraMap K L E.a₃)⟩, ?_, ?_⟩  · rw [variableChange_def]    ext <;>      simp only [quadraticTwistBy, quadraticTwistOf, baseChange, map_a₁, map_a₂, map_a₃,        map_a₄, map_a₆, Units.val_inv_eq_inv_val, Units.val_mk0, map_sub, map_mul,        map_pow, map_ofNat, hT, hN] <;>      field  · ext <;>      simp only [VariableChange.map, VariableChange.mul_def, negVariableChange, Units.coe_map,        Units.val_mul, Units.val_neg, Units.val_one, Units.val_mk0, hap, MonoidHom.coe_coe,        map_neg, map_mul, map_pow, map_sub, map_zero, map_a₁, map_a₃, baseChange,        σ.commutes, hσσ] <;>      ring