Lean4
theorem XYIdeal_mul_XYIdeal [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
XIdeal W (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) * (XYIdeal W x₁ (C y₁) * XYIdeal W x₂ (C y₂)) =
YIdeal W (linePolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) *
XYIdeal W (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (C <| W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
by
have sup_rw : ∀ a b c d : Ideal W.CoordinateRing, a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c := fun _ _ c _ => by
rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]
rw [XYIdeal_add_eq, XIdeal, mul_comm, XYIdeal_eq₁ x₁ y₁ <| W.slope x₁ x₂ y₁ y₂, XYIdeal, XYIdeal_eq₂ h₁ h₂ hxy,
XYIdeal, span_pair_mul_span_pair]
simp_rw [span_insert, sup_rw, Ideal.sup_mul, span_singleton_mul_span_singleton]
rw [← neg_eq_iff_eq_neg.mpr <| C_addPolynomial_slope h₁ h₂ hxy, span_singleton_neg, C_addPolynomial, map_mul, YClass]
simp_rw [mul_comm <| XClass W x₁, mul_assoc, ← span_singleton_mul_span_singleton, ← Ideal.mul_sup]
rw [span_singleton_mul_span_singleton, ← span_insert, ←
span_pair_add_mul_right <| -(XClass W <| W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂), mul_neg, ← sub_eq_add_neg, ← sub_mul,
← map_sub <| mk W, sub_sub_sub_cancel_right, span_insert, ← span_singleton_mul_span_singleton, ← sup_rw, ←
Ideal.sup_mul, ← Ideal.sup_mul]
apply congr_arg (_ ∘ _)
convert top_mul (_ : Ideal W.CoordinateRing)
simp_rw [XClass, ← Set.image_singleton (f := mk W), ← map_span, ← Ideal.map_sup, eq_top_iff_one,
mem_map_iff_of_surjective _ AdjoinRoot.mk_surjective, ← span_insert, mem_span_insert', mem_span_singleton']
by_cases hx : x₁ = x₂
· have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
let y := (y₁ - W.negY x₁ y₁) ^ 2
replace hxy := pow_ne_zero 2 <| sub_ne_zero_of_ne hy
refine
⟨1 + C (C <| y⁻¹ * 4) * W.polynomial,
⟨C <| C y⁻¹ * (C 4 * X ^ 2 + C (4 * x₁ + W.b₂) * X + C (4 * x₁ ^ 2 + W.b₂ * x₁ + 2 * W.b₄)), 0,
C (C y⁻¹) * (Y - W.negPolynomial), ?_⟩,
by rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]⟩
rw [polynomial, negPolynomial, ← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hxy]
simp only [y, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hxy]
linear_combination (norm := (rw [b₂, b₄, negY]; C_simp; ring1))
-4 * congr_arg C (congr_arg C <| (equation_iff ..).mp h₁)
· replace hx := sub_ne_zero_of_ne hx
refine ⟨_, ⟨⟨C <| C (x₁ - x₂)⁻¹, C <| C <| (x₁ - x₂)⁻¹ * -1, 0, ?_⟩, map_one _⟩⟩
rw [← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hx]
simp only [← mul_assoc, mul_add, ← C_mul, mul_inv_cancel₀ hx]
C_simp
ring1