awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
s : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
⊢ x.s = x_1.s

Tactic:
apply_fun _ using hφ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
t : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
⊢ x.t = x_1.t

Tactic:
apply_fun _ using hφ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
⊢ Eq.{v + 1} (α := A) ((φ : (a : R) → A) (↑x.u : R) : A) ((φ : (a : R) → A) (↑x_1.u : R) : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
⊢ Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
⊢ Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
⊢ Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
simp :
  Eq (α := VariableChange A)
    ({ u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      VariableChange A)
    ({ u := 1, r := 0, s := 0, t := 0 } : VariableChange A)
⊢ map 1 φ = 1

Tactic:
simp only [one_def, map]

Premises used: WeierstrassCurve.VariableChange.one_def, WeierstrassCurve.VariableChange.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
u :
  Eq (α := A)
    ((↑(VariableChange.u
            { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
              s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 }) :
        A) :
      A)
    ((↑(VariableChange.u { u := 1, r := 0, s := 0, t := 0 }) : A) : A)
r :
  Eq (α := A)
    (VariableChange.r
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (VariableChange.r { u := 1, r := 0, s := 0, t := 0 } : A)
s :
  Eq (α := A)
    (VariableChange.s
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (VariableChange.s { u := 1, r := 0, s := 0, t := 0 } : A)
t :
  Eq (α := A)
    (VariableChange.t
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (VariableChange.t { u := 1, r := 0, s := 0, t := 0 } : A)
⊢ Eq (α := VariableChange A)
    ({ u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      VariableChange A)
    ({ u := 1, r := 0, s := 0, t := 0 } : VariableChange A)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
⊢ Eq (α := A)
    ((↑(u
            { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
              s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 }) :
        A) :
      A)
    ((↑(u { u := 1, r := 0, s := 0, t := 0 }) : A) : A)

Tactic:
simp only [map_one, Units.val_one, map_zero]

Premises used: map_zero, map_one, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
⊢ Eq (α := A)
    (r
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (r { u := 1, r := 0, s := 0, t := 0 } : A)

Tactic:
simp only [map_one, Units.val_one, map_zero]

Premises used: map_zero, map_one, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
⊢ Eq (α := A)
    (s
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (s { u := 1, r := 0, s := 0, t := 0 } : A)

Tactic:
simp only [map_one, Units.val_one, map_zero]

Premises used: map_zero, map_one, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
⊢ Eq (α := A)
    (t
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (t { u := 1, r := 0, s := 0, t := 0 } : A)

Tactic:
simp only [map_one, Units.val_one, map_zero]

Premises used: map_zero, map_one, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
simp :
  { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
      r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
      s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
      t :=
        (φ : (a : R) → A)
          (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) } =
    {
      u :=
        HMul.hMul (α := Aˣ) (β := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
          (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
      r :=
        HAdd.hAdd (β := A)
          (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
            (HPow.hPow (α := A) (β := ℕ)
              (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
          ((φ : (a : R) → A) C'.r : A),
      s :=
        HAdd.hAdd (β := A)
          (HMul.hMul (α := A) (β := A)
            ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
            ((φ : (a : R) → A) C.s : A))
          ((φ : (a : R) → A) C'.s : A),
      t :=
        HAdd.hAdd (β := A)
          (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
              (HPow.hPow (α := A) (β := ℕ)
                (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
            HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
              HPow.hPow (α := A) (β := ℕ)
                (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
          ((φ : (a : R) → A) C'.t : A) :
      VariableChange A }
⊢ (C * C').map φ = C.map φ * C'.map φ

Tactic:
simp only [mul_def, map]

Premises used: WeierstrassCurve.VariableChange.mul_def, WeierstrassCurve.VariableChange.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ (↑(u
          { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
            r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
            s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
            t :=
              (φ : (a : R) → A)
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) }) :
      A) =
    (↑{
            u :=
              HMul.hMul (α := Aˣ) (β := Aˣ)
                (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
                (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
            r :=
              HAdd.hAdd (β := A)
                (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
                  (HPow.hPow (α := A) (β := ℕ)
                    (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
                ((φ : (a : R) → A) C'.r : A),
            s :=
              HAdd.hAdd (β := A)
                (HMul.hMul (α := A) (β := A)
                  ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
                  ((φ : (a : R) → A) C.s : A))
                ((φ : (a : R) → A) C'.s : A),
            t :=
              HAdd.hAdd (β := A)
                (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
                    (HPow.hPow (α := A) (β := ℕ)
                      (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
                  HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
                    HPow.hPow (α := A) (β := ℕ)
                      (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
                ((φ : (a : R) → A) C'.t : A) :
            VariableChange A }.u :
      A)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
r :
  HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
        (HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C'.u : R) : A) 2))
      ((φ : (a : R) → A) C'.r : A) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
        (HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A)
          2))
      ((φ : (a : R) → A) C'.r : A)
⊢ VariableChange.r
      { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
        r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
        s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
        t :=
          (φ : (a : R) → A)
            (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) } =
    {
        u :=
          HMul.hMul (α := Aˣ) (β := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
            (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
        r :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
              (HPow.hPow (α := A) (β := ℕ)
                (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
            ((φ : (a : R) → A) C'.r : A),
        s :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) (β := A)
              ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
              ((φ : (a : R) → A) C.s : A))
            ((φ : (a : R) → A) C'.s : A),
        t :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
                (HPow.hPow (α := A) (β := ℕ)
                  (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
              HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
                HPow.hPow (α := A) (β := ℕ)
                  (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
            ((φ : (a : R) → A) C'.t : A) :
        VariableChange A }.r

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
s :
  HAdd.hAdd (β := A) (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) (↑C'.u : R) : A) ((φ : (a : R) → A) C.s : A))
      ((φ : (a : R) → A) C'.s : A) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := A) (β := A)
        ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
        ((φ : (a : R) → A) C.s : A))
      ((φ : (a : R) → A) C'.s : A)
⊢ VariableChange.s
      { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
        r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
        s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
        t :=
          (φ : (a : R) → A)
            (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) } =
    {
        u :=
          HMul.hMul (α := Aˣ) (β := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
            (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
        r :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
              (HPow.hPow (α := A) (β := ℕ)
                (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
            ((φ : (a : R) → A) C'.r : A),
        s :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) (β := A)
              ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
              ((φ : (a : R) → A) C.s : A))
            ((φ : (a : R) → A) C'.s : A),
        t :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
                (HPow.hPow (α := A) (β := ℕ)
                  (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
              HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
                HPow.hPow (α := A) (β := ℕ)
                  (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
            ((φ : (a : R) → A) C'.t : A) :
        VariableChange A }.s

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
t :
  HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
          (HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C'.u : R) : A) 3) +
        HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
          HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C'.u : R) : A) 2)
      ((φ : (a : R) → A) C'.t : A) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
          (HPow.hPow (α := A) (β := ℕ)
            (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
        HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
          HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A)
            2)
      ((φ : (a : R) → A) C'.t : A)
⊢ VariableChange.t
      { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
        r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
        s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
        t :=
          (φ : (a : R) → A)
            (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) } =
    {
        u :=
          HMul.hMul (α := Aˣ) (β := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
            (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
        r :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
              (HPow.hPow (α := A) (β := ℕ)
                (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
            ((φ : (a : R) → A) C'.r : A),
        s :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) (β := A)
              ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
              ((φ : (a : R) → A) C.s : A))
            ((φ : (a : R) → A) C'.s : A),
        t :=
          HAdd.hAdd (β := A)
            (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
                (HPow.hPow (α := A) (β := ℕ)
                  (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
              HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
                HPow.hPow (α := A) (β := ℕ)
                  (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
            ((φ : (a : R) → A) C'.t : A) :
        VariableChange A }.t

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
        (HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C'.u : R) : A) 2))
      ((φ : (a : R) → A) C'.r : A) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
        (HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A)
          2))
      ((φ : (a : R) → A) C'.r : A)

Tactic:
simp only [Units.coe_map, MonoidHom.coe_coe]

Premises used: Units.coe_map, MonoidHom.coe_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ HAdd.hAdd (β := A) (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) (↑C'.u : R) : A) ((φ : (a : R) → A) C.s : A))
      ((φ : (a : R) → A) C'.s : A) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := A) (β := A)
        ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
        ((φ : (a : R) → A) C.s : A))
      ((φ : (a : R) → A) C'.s : A)

Tactic:
simp only [Units.coe_map, MonoidHom.coe_coe]

Premises used: Units.coe_map, MonoidHom.coe_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
          (HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C'.u : R) : A) 3) +
        HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
          HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C'.u : R) : A) 2)
      ((φ : (a : R) → A) C'.t : A) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
          (HPow.hPow (α := A) (β := ℕ)
            (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
        HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
          HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A)
            2)
      ((φ : (a : R) → A) C'.t : A)

Tactic:
simp only [Units.coe_map, MonoidHom.coe_coe]

Premises used: Units.coe_map, MonoidHom.coe_coe