Exists smul eq or exists smul eq quadratic Twist

theorem exists_smul_eq_or_exists_smul_eq_quadraticTwist (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728)    (E' : WeierstrassCurve K)    (h : ∃ C : VariableChange L, C • E'.baseChange L = E.baseChange L) :    (∃ C : VariableChange K, C • E' = E) ∨ ∃ C : VariableChange K, C • E' = E.quadraticTwist L := by  obtain ⟨ρ, hρ⟩ := h  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σ  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₁₇₂₈  have hmapmul : ∀ a b : VariableChange L, (a * b).map σ.toAlgHom.toRingHom      = a.map σ.toAlgHom.toRingHom * b.map σ.toAlgHom.toRingHom :=    fun a b ↦ map_mul (VariableChange.mapHom σ.toAlgHom.toRingHom) a b  have hmapinv : ∀ a : VariableChange L, a⁻¹.map σ.toAlgHom.toRingHom      = (a.map σ.toAlgHom.toRingHom)⁻¹ :=    fun a ↦ map_inv (VariableChange.mapHom σ.toAlgHom.toRingHom) a  -- The Galois conjugate `σρ = ρ.map σ` is again an isomorphism `E'ᴸ ≅ Eᴸ`  -- (`map_smul_baseChange_eq`).  have hσρ : (ρ.map σ.toAlgHom.toRingHom) • E'.baseChange L = E.baseChange L :=    map_smul_baseChange_eq L σ hρ  -- Hence `b := σρ · ρ⁻¹` is an automorphism of `Eᴸ`, so `b = 1` or `b = [-1]`.  have hρinv : ρ⁻¹ • E.baseChange L = E'.baseChange L := by rw [← hρ, inv_smul_smul]  have hb : (ρ.map σ.toAlgHom.toRingHom * ρ⁻¹) • E.baseChange L = E.baseChange L := by    rw [mul_smul, hρinv, hσρ]  rcases (E.baseChange L).eq_one_or_eq_negVariableChange_of_smul_eq_of_c₄_ne_zero hc4L hc6L hb    with hbcase | hbcase  · -- Trivial cocycle: `ρ` is `σ`-invariant, descends, and `E' ≅ E` over `K`.    left    have hρmap : ρ.map σ.toAlgHom.toRingHom = ρ := mul_inv_eq_one.mp hbcase    obtain ⟨ρK, hρK⟩ := exists_baseChange_eq_of_map_eq L hσ hρmap    exact ⟨ρK, smul_eq_of_baseChange_smul_eq L ρK (by rw [hρK]; exact hρ)⟩  · -- Nontrivial cocycle: `χ := C₁⁻¹ · ρ` is `σ`-invariant (its cocycle cancels that of `C₁`),    -- descends, and `E' ≅ Eᶿ`, hence `E' ≅ Eᴸ` after the harmless change of generator.    right    have hρmap : ρ.map σ.toAlgHom.toRingHom = (E.baseChange L).negVariableChange * ρ :=      mul_inv_eq_iff_eq_mul.mp hbcase    have hC1inv : C₁⁻¹ • E.baseChange L = (E.quadraticTwistBy θ).baseChange L := by      rw [← hiso, inv_smul_smul]    have hχiso : (C₁⁻¹ * ρ) • E'.baseChange L = (E.quadraticTwistBy θ).baseChange L := by      rw [mul_smul, hρ, hC1inv]    have hχinv : (C₁⁻¹ * ρ).map σ.toAlgHom.toRingHom = C₁⁻¹ * ρ := by      rw [hmapmul, hmapinv, hcoc, hρmap, mul_inv_rev, (E.baseChange L).negVariableChange_inv]      have hnn : (E.baseChange L).negVariableChange          * ((E.baseChange L).negVariableChange * ρ) = ρ := by        rw [← mul_assoc, (E.baseChange L).negVariableChange_mul_self, one_mul]      rw [mul_assoc, hnn]    obtain ⟨χK, hχK⟩ := exists_baseChange_eq_of_map_eq L hσ hχinv    have hE'Tby : χK • E' = E.quadraticTwistBy θ :=      smul_eq_of_baseChange_smul_eq L χK (by rw [hχK]; exact hχiso)    obtain ⟨C₀, hC₀⟩ := E.exists_smul_quadraticTwist_eq_quadraticTwistBy L hθ    refine ⟨C₀⁻¹ * χK, ?_⟩    rw [mul_smul, hE'Tby, ← hC₀, inv_smul_smul]