Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case a₂
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 2 *
      (W.a₂ - (↑C'.u * C.s + C'.s) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) - (↑C'.u * C.s + C'.s) ^ 2) =
    ↑C.u⁻¹ ^ 2 *
      (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2) - C.s * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r -
        C.s ^ 2)

pp: case a₃
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 3 *
      (W.a₃ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₁ + 2 * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) =
    ↑C.u⁻¹ ^ 3 * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) + C.r * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 2 * C.t)

pp: case a₄
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 4 *
      (W.a₄ - (↑C'.u * C.s + C'.s) * W.a₃ + 2 * (C.r * ↑C'.u ^ 2 + C'.r) * W.a₂ -
            (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t + (C.r * ↑C'.u ^ 2 + C'.r) * (↑C'.u * C.s + C'.s)) * W.a₁ +
          3 * (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 -
        2 * (↑C'.u * C.s + C'.s) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) =
    ↑C.u⁻¹ ^ 4 *
      (↑C'.u⁻¹ ^ 4 *
                  (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                    2 * C'.s * C'.t) -
                C.s * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) +
              2 * C.r * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) -
            (C.t + C.r * C.s) * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) +
          3 * C.r ^ 2 -
        2 * C.s * C.t)

pp: case a₆
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 6 *
      (W.a₆ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₄ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 * W.a₂ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 3 -
            (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₃ -
          (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) ^ 2 -
        (C.r * ↑C'.u ^ 2 + C'.r) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₁) =
    ↑C.u⁻¹ ^ 6 *
      (↑C'.u⁻¹ ^ 6 * (W.a₆ + C'.r * W.a₄ + C'.r ^ 2 * W.a₂ + C'.r ^ 3 - C'.t * W.a₃ - C'.t ^ 2 - C'.r * C'.t * W.a₁) +
                  C.r *
                    (↑C'.u⁻¹ ^ 4 *
                      (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                        2 * C'.s * C'.t)) +
                C.r ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) +
              C.r ^ 3 -
            C.t * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) -
          C.t ^ 2 -
        C.r * C.t * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)))

Tactic:
· linear_combination
        C.s * (-C'.s * 2 - W.a₁) * C.u⁻¹ ^ 2 * ↑C'.u⁻¹ * C'.u.inv_mul
          + (C.r * 3 - C.s ^ 2) * C.u⁻¹ ^ 2 * pow_mul_pow_eq_one 2 C'.u.inv_mul

Goal state after:
case a₃
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 3 *
      (W.a₃ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₁ + 2 * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) =
    ↑C.u⁻¹ ^ 3 * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) + C.r * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 2 * C.t)

case a₄
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 4 *
      (W.a₄ - (↑C'.u * C.s + C'.s) * W.a₃ + 2 * (C.r * ↑C'.u ^ 2 + C'.r) * W.a₂ -
            (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t + (C.r * ↑C'.u ^ 2 + C'.r) * (↑C'.u * C.s + C'.s)) * W.a₁ +
          3 * (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 -
        2 * (↑C'.u * C.s + C'.s) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) =
    ↑C.u⁻¹ ^ 4 *
      (↑C'.u⁻¹ ^ 4 *
                  (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                    2 * C'.s * C'.t) -
                C.s * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) +
              2 * C.r * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) -
            (C.t + C.r * C.s) * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) +
          3 * C.r ^ 2 -
        2 * C.s * C.t)

case a₆
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 6 *
      (W.a₆ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₄ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 * W.a₂ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 3 -
            (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₃ -
          (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) ^ 2 -
        (C.r * ↑C'.u ^ 2 + C'.r) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₁) =
    ↑C.u⁻¹ ^ 6 *
      (↑C'.u⁻¹ ^ 6 * (W.a₆ + C'.r * W.a₄ + C'.r ^ 2 * W.a₂ + C'.r ^ 3 - C'.t * W.a₃ - C'.t ^ 2 - C'.r * C'.t * W.a₁) +
                  C.r *
                    (↑C'.u⁻¹ ^ 4 *
                      (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                        2 * C'.s * C'.t)) +
                C.r ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) +
              C.r ^ 3 -
            C.t * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) -
          C.t ^ 2 -
        C.r * C.t * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)))