awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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
      { 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
have 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: map_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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
      { 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
have 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)
Tactic: map_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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
      { 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
have 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)
Tactic: map_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ 4 * W.b₈ = W.b₂ * W.b₆ - HPow.hPow (β := ℕ) W.b₄ 2
have simp : 4 *
    (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
      HPow.hPow (β := ℕ) W.a₄ 2) =
  (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) -
    HPow.hPow (β := ℕ) (2 * W.a₄ + W.a₁ * W.a₃) 2
Tactic: simp only [b₂, b₄, b₆, b₈]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ 1728 * W.Δ = HPow.hPow (β := ℕ) W.c₄ 3 - HPow.hPow (β := ℕ) W.c₆ 2
have simp : 1728 *
    (-HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 2 *
            (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ +
                W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
              HPow.hPow (β := ℕ) W.a₄ 2) -
          8 * HPow.hPow (β := ℕ) (2 * W.a₄ + W.a₁ * W.a₃) 3 -
        27 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) 2 +
      9 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆)) =
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 2 - 24 * (2 * W.a₄ + W.a₁ * W.a₃)) 3 -
    HPow.hPow (β := ℕ)
      (-HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 3 +
          36 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) -
        216 * (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆))
      2
Tactic: simp only [b₂, b₄, b₆, b₈, c₄, c₆, Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.b₂ = HPow.hPow (β := ℕ) W.a₁ 2
have rw : HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ = HPow.hPow (β := ℕ) W.a₁ 2
Tactic: rw [b₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.b₄ = W.a₁ * W.a₃
have rw : 2 * W.a₄ + W.a₁ * W.a₃ = W.a₁ * W.a₃
Tactic: rw [b₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.b₆ = HPow.hPow (β := ℕ) W.a₃ 2
have rw : HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆ = HPow.hPow (β := ℕ) W.a₃ 2
Tactic: rw [b₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.b₈ =
    HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 + HPow.hPow (β := ℕ) W.a₄ 2
have rw : HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
    HPow.hPow (β := ℕ) W.a₄ 2 =
  HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 + HPow.hPow (β := ℕ) W.a₄ 2
Tactic: rw [b₈]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.c₄ = HPow.hPow (β := ℕ) W.a₁ 4
have rw : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2) 2 - 24 * W.b₄ = HPow.hPow (β := ℕ) W.a₁ 4
Tactic: rw [c₄, b₂_of_char_two]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.c₆ = HPow.hPow (β := ℕ) W.a₁ 6
have rw : -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2) 3 + 36 * HPow.hPow (β := ℕ) W.a₁ 2 * W.b₄ - 216 * W.b₆ =
  HPow.hPow (β := ℕ) W.a₁ 6
Tactic: rw [c₆, b₂_of_char_two]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.Δ =
    HPow.hPow (β := ℕ) W.a₁ 4 * W.b₈ + HPow.hPow (β := ℕ) W.a₃ 4 + HPow.hPow (β := ℕ) W.a₁ 3 * HPow.hPow (β := ℕ) W.a₃ 3
have rw : -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2) 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) (W.a₁ * W.a₃) 3 -
      27 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₃ 2) 2 +
    9 * HPow.hPow (β := ℕ) W.a₁ 2 * (W.a₁ * W.a₃) * HPow.hPow (β := ℕ) W.a₃ 2 =
  HPow.hPow (β := ℕ) W.a₁ 4 * W.b₈ + HPow.hPow (β := ℕ) W.a₃ 4 + HPow.hPow (β := ℕ) W.a₁ 3 * HPow.hPow (β := ℕ) W.a₃ 3
Tactic: rw [Δ, b₂_of_char_two, b₄_of_char_two, b₆_of_char_two]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.b₂ = HPow.hPow (β := ℕ) W.a₁ 2 + W.a₂
have rw : HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ = HPow.hPow (β := ℕ) W.a₁ 2 + W.a₂
Tactic: rw [b₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.b₄ = -W.a₄ + W.a₁ * W.a₃
have rw : 2 * W.a₄ + W.a₁ * W.a₃ = -W.a₄ + W.a₁ * W.a₃
Tactic: rw [b₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.b₆ = HPow.hPow (β := ℕ) W.a₃ 2 + W.a₆
have rw : HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆ = HPow.hPow (β := ℕ) W.a₃ 2 + W.a₆
Tactic: rw [b₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.b₈ =
    HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
      HPow.hPow (β := ℕ) W.a₄ 2
have rw : HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
    HPow.hPow (β := ℕ) W.a₄ 2 =
  HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
    HPow.hPow (β := ℕ) W.a₄ 2
Tactic: rw [b₈]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.c₄ = HPow.hPow (β := ℕ) W.b₂ 2
have rw : HPow.hPow (β := ℕ) W.b₂ 2 - 24 * W.b₄ = HPow.hPow (β := ℕ) W.b₂ 2
Tactic: rw [c₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.c₆ = -HPow.hPow (β := ℕ) W.b₂ 3
have rw : -HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆ = -HPow.hPow (β := ℕ) W.b₂ 3
Tactic: rw [c₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.Δ = -HPow.hPow (β := ℕ) W.b₂ 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) W.b₄ 3
have rw : -HPow.hPow (β := ℕ) W.b₂ 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) W.b₄ 3 - 27 * HPow.hPow (β := ℕ) W.b₆ 2 +
    9 * W.b₂ * W.b₄ * W.b₆ =
  -HPow.hPow (β := ℕ) W.b₂ 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) W.b₄ 3
Tactic: rw [Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ (W.map f).b₂ = (f : (a : R) → A) W.b₂
have simp : HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₁ : A) 2 +
    HMul.hMul (α := A) (β := A) (4 : A) ((f : (a : R) → A) W.a₂ : A) =
  (f : (a : R) → A) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂)
Tactic: simp only [b₂, map_a₁, map_a₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ (W.map f).b₄ = (f : (a : R) → A) W.b₄
have simp : HMul.hMul (α := A) (β := A) (2 : A) ((f : (a : R) → A) W.a₄ : A) +
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) W.a₁ : A) ((f : (a : R) → A) W.a₃ : A) =
  (f : (a : R) → A) (2 * W.a₄ + W.a₁ * W.a₃)
Tactic: simp only [b₄, map_a₁, map_a₃, map_a₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ (W.map f).b₆ = (f : (a : R) → A) W.b₆
have simp : HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₃ : A) 2 +
    HMul.hMul (α := A) (β := A) (4 : A) ((f : (a : R) → A) W.a₆ : A) =
  (f : (a : R) → A) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆)
Tactic: simp only [b₆, map_a₃, map_a₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ (W.map f).b₈ = (f : (a : R) → A) W.b₈
have simp : HMul.hMul (β := A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₁ : A) 2) ((f : (a : R) → A) W.a₆ : A) +
          HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (4 : A) ((f : (a : R) → A) W.a₂ : A))
            ((f : (a : R) → A) W.a₆ : A) -
        HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) ((f : (a : R) → A) W.a₁ : A) ((f : (a : R) → A) W.a₃ : A))
          ((f : (a : R) → A) W.a₄ : A) +
      HMul.hMul (α := A) ((f : (a : R) → A) W.a₂ : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₃ : A) 2) -
    HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₄ : A) 2 =
  (f : (a : R) → A)
    (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
      HPow.hPow (β := ℕ) W.a₄ 2)
Tactic: simp only [b₈, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ (W.map f).c₄ = (f : (a : R) → A) W.c₄
have simp : HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 2 -
    HMul.hMul (α := A) (β := A) (24 : A) ((f : (a : R) → A) W.b₄ : A) =
  (f : (a : R) → A) (HPow.hPow (β := ℕ) W.b₂ 2 - 24 * W.b₄)
Tactic: simp only [c₄, map_b₂, map_b₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ (W.map f).c₆ = (f : (a : R) → A) W.c₆
have simp : -HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 3 +
      HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (36 : A) ((f : (a : R) → A) W.b₂ : A))
        ((f : (a : R) → A) W.b₄ : A) -
    HMul.hMul (α := A) (β := A) (216 : A) ((f : (a : R) → A) W.b₆ : A) =
  (f : (a : R) → A) (-HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)
Tactic: simp only [c₆, map_b₂, map_b₄, map_b₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ (W.map f).Δ = (f : (a : R) → A) W.Δ
have simp : HMul.hMul (β := A) (-HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 2) ((f : (a : R) → A) W.b₈ : A) -
        8 * HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₄ : A) 3 -
      27 * HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₆ : A) 2 +
    HMul.hMul (β := A)
      (HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (9 : A) ((f : (a : R) → A) W.b₂ : A))
        ((f : (a : R) → A) W.b₄ : A))
      ((f : (a : R) → A) W.b₆ : A) =
  (f : (a : R) → A)
    (-HPow.hPow (β := ℕ) W.b₂ 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) W.b₄ 3 - 27 * HPow.hPow (β := ℕ) W.b₆ 2 +
      9 * W.b₂ * W.b₄ * W.b₆)
Tactic: simp only [Δ, map_b₂, map_b₄, map_b₆, map_b₈]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
⊢ x = x_1
have left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
Tactic: rcases mk.inj h with ⟨_, _, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
⊢ x = x_1
have left₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
Tactic: rcases mk.inj h with ⟨_, _, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
⊢ x = x_1
have left₂ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
Tactic: rcases mk.inj h with ⟨_, _, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left₂ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
⊢ x = x_1
have left₃ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
Tactic: rcases mk.inj h with ⟨_, _, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left₂ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left₃ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
⊢ x = x_1
have right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
Tactic: rcases mk.inj h with ⟨_, _, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ x = x_1
have a₁ : x.a₁ = x_1.a₁
Tactic: ext