Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ ↑{ u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
          t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.u =
    ↑{ u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
          s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
          t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.u

pp: case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.r =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.r

pp: case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.s =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.s

pp: case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.t =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.t

Tactic:
<;>

Goal state after:
case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ ↑{ u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
          t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.u =
    ↑{ u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
          s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
          t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.u

case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.r =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.r

case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.s =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.s

case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.t =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.t