Has Multiplicative Reduction base Change quadratic Twist Of

theorem hasMultiplicativeReduction_baseChange_quadraticTwistOf [E.HasMultiplicativeReduction R]    (t n : R) (hD : residue R (t ^ 2 - 4 * n) ≠ 0) :    (((E.integralModel R).quadraticTwistOf t n)⁄K).HasMultiplicativeReduction R := by  set W := (E.integralModel R).quadraticTwistOf t n with hW  have hWint : IsIntegral R (W⁄K) := ⟨⟨W, rfl⟩⟩  -- `residue W.c₄ = residue D² · residue (E.integralModel R).c₄ ≠ 0`, `residue W.Δ = 0`.  have hc₄res : residue R W.c₄ ≠ 0 := by    rw [hW, c₄_quadraticTwistOf, map_mul, map_pow]    exact mul_ne_zero (pow_ne_zero 2 hD) (residue_integralModel_c₄_ne_zero E R)  have hΔres : residue R W.Δ = 0 := by    rw [hW, Δ_quadraticTwistOf, map_mul, map_pow, residue_integralModel_Δ_eq_zero E R, mul_zero]  -- Convert to the valuation conditions on the base change `W⁄K`.  have hc₄val : valuation K (IsDiscreteValuationRing.maximalIdeal R) (W⁄K).c₄ = 1 := by    rw [show (W⁄K).c₄ = algebraMap R K W.c₄ from map_c₄ W (algebraMap R K)]    exact (IsDiscreteValuationRing.maximalIdeal R).valuation_eq_one_iff_notMem.mpr      fun hmem ↦ hc₄res ((residue_eq_zero_iff W.c₄).mpr hmem)  have hΔval : valuation K (IsDiscreteValuationRing.maximalIdeal R) (W⁄K).Δ < 1 := by    rw [show (W⁄K).Δ = algebraMap R K W.Δ from map_Δ W (algebraMap R K)]    exact ((IsDiscreteValuationRing.maximalIdeal R).valuation_lt_one_iff_mem W.Δ).mpr      ((residue_eq_zero_iff W.Δ).mp hΔres)  have : IsMinimal R (W⁄K) := isMinimal_of_valuation_c₄_eq_one R (W⁄K) hc₄val  exact { badReduction := hΔval, multiplicativeReduction := hc₄val }