Not exists smul quadratic Twist eq

theorem not_exists_smul_quadraticTwist_eq (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728) :    ¬∃ C : VariableChange K, C • E.quadraticTwist L = E := by  rintro ⟨CK, hCK⟩  obtain ⟨σ, hσ⟩ := exists_algEquiv_ne_one K L  obtain ⟨θ, hθ⟩ := exists_notMem_range_algebraMap K L  obtain ⟨C₁, hiso, hcoc⟩ := E.exists_smul_baseChange_and_map_eq L hθ hσ  obtain ⟨C₀, hC₀⟩ := E.exists_smul_quadraticTwist_eq_quadraticTwistBy L hθ  -- Transfer the hypothetical `K`-isomorphism to the twist by `θ`.  have hDK : (CK * C₀⁻¹) • E.quadraticTwistBy θ = E := by    rw [mul_smul, ← hC₀, inv_smul_smul, hCK]  -- Base change it: a `σ`-invariant `L`-isomorphism `(Eᶿ)ᴸ ≅ Eᴸ`.  set ψ := (CK * C₀⁻¹).baseChange L with hψ  have hψiso : ψ • (E.quadraticTwistBy θ).baseChange L = E.baseChange L := by    rw [hψ, baseChange_smul_baseChange, hDK]  have hψinv : ψ.map σ.toAlgHom.toRingHom = ψ := by    rw [hψ]; exact VariableChange.map_baseChange (C := CK * C₀⁻¹) σ.toAlgHom  -- `c₄, c₆` of `Eᴸ` are nonzero, so `Aut(Eᴸ) = {±1}`.  have hc4L : (E.baseChange L).c₄ ≠ 0 := E.baseChange_c₄_ne_zero L hj₀  have hc6L : (E.baseChange L).c₆ ≠ 0 := E.baseChange_c₆_ne_zero L hj₁₇₂₈  -- `a := ψ · C₁⁻¹` is an automorphism of `Eᴸ`, so `a = 1` or `a = [-1]`.  set a := ψ * C₁⁻¹ with ha  have hC1inv : C₁⁻¹ • E.baseChange L = (E.quadraticTwistBy θ).baseChange L := by    rw [← hiso, inv_smul_smul]  have haut : a • E.baseChange L = E.baseChange L := by    rw [ha, mul_smul, hC1inv, hψiso]  have haC : a * C₁ = ψ := by rw [ha, mul_assoc, inv_mul_cancel, mul_one]  have hamap : a.map σ.toAlgHom.toRingHom = a := by    rcases (E.baseChange L).eq_one_or_eq_negVariableChange_of_smul_eq_of_c₄_ne_zero hc4L hc6L haut      with hcase | hcase    · rw [hcase]; exact map_one (VariableChange.mapHom σ.toAlgHom.toRingHom)    · rw [hcase]; exact E.negVariableChange_baseChange_map L σ  -- Applying `σ` to `ψ = a · C₁` forces `[-1] = 1`, a contradiction.  apply (E.baseChange L).negVariableChange_ne_one  have hchain : a * ((E.baseChange L).negVariableChange * C₁) = a * C₁ :=    calc a * ((E.baseChange L).negVariableChange * C₁)        = a.map σ.toAlgHom.toRingHom * C₁.map σ.toAlgHom.toRingHom := by rw [hamap, hcoc]      _ = (a * C₁).map σ.toAlgHom.toRingHom :=          (map_mul (VariableChange.mapHom σ.toAlgHom.toRingHom) a C₁).symm      _ = ψ.map σ.toAlgHom.toRingHom := by rw [haC]      _ = ψ := hψinv      _ = a * C₁ := haC.symm  have : (E.baseChange L).negVariableChange * C₁ = C₁ := mul_left_cancel hchain  exact mul_right_cancel (this.trans (one_mul C₁).symm)