Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * s ^ 2 +
              C (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * s * t +
            C (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * s * u +
          C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t ^ 2 +
        C (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * t * u).IsHomogeneous
    2

pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * s ^ 2 +
          C (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * s * t +
        C (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * s * u).IsHomogeneous
    2

pp: case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

pp: case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
· exact CXX.add CXY |>.add CXY |>.add CXX |>.add CXY

Goal state after:
case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * s ^ 2 +
          C (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * s * t +
        C (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * s * u).IsHomogeneous
    2

case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2