Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑{ u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
          r :=
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r *
                ↑C.u ^ 2 +
              C.r,
          s :=
            ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
              C.s,
          t :=
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t *
                  ↑C.u ^ 3 +
                { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r *
                    C.s *
                  ↑C.u ^ 2 +
              C.t }.u =
    ↑{ u := 1, r := 0, s := 0, t := 0 }.u

pp: case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.r =
    { u := 1, r := 0, s := 0, t := 0 }.r

pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.s =
    { u := 1, r := 0, s := 0, t := 0 }.s

pp: case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.t =
    { u := 1, r := 0, s := 0, t := 0 }.t

Tactic:
<;>

Goal state after:
case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑{ u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
          r :=
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r *
                ↑C.u ^ 2 +
              C.r,
          s :=
            ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
              C.s,
          t :=
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t *
                  ↑C.u ^ 3 +
                { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r *
                    C.s *
                  ↑C.u ^ 2 +
              C.t }.u =
    ↑{ u := 1, r := 0, s := 0, t := 0 }.u

case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.r =
    { u := 1, r := 0, s := 0, t := 0 }.r

case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.s =
    { u := 1, r := 0, s := 0, t := 0 }.s

case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.t =
    { u := 1, r := 0, s := 0, t := 0 }.t