awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A) *
      HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₁ : A)
        (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.s : A)) =
    HMul.hMul (α := A) ((φ : (a : R) → A) (↑C.u⁻¹ : R) : A)
      (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₁ : A)
        (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.s : A)))

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

Premises used: Units.coe_map_inv, MonoidHom.coe_coe
-- 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
⊢ HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A) 2 *
      (HSub.hSub (α := A) ((φ : (a : R) → A) W.a₂ : A)
            (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.s : A) ((φ : (a : R) → A) W.a₁ : A)) +
          HMul.hMul (α := A) (β := A) (3 : A) ((φ : (a : R) → A) C.r : A) -
        HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.s : A) 2) =
    HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C.u⁻¹ : R) : A) 2 *
      (HSub.hSub (α := A) ((φ : (a : R) → A) W.a₂ : A)
            (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.s : A) ((φ : (a : R) → A) W.a₁ : A)) +
          HMul.hMul (α := A) (β := A) (3 : A) ((φ : (a : R) → A) C.r : A) -
        HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.s : A) 2)

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

Premises used: Units.coe_map_inv, MonoidHom.coe_coe
-- 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
⊢ HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A) 3 *
      (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₃ : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) W.a₁ : A)) +
        HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.t : A)) =
    HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C.u⁻¹ : R) : A) 3 *
      (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₃ : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) W.a₁ : A)) +
        HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.t : A))

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

Premises used: Units.coe_map_inv, MonoidHom.coe_coe
-- 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
⊢ HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A) 4 *
      (HSub.hSub (α := A) ((φ : (a : R) → A) W.a₄ : A)
                (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.s : A) ((φ : (a : R) → A) W.a₃ : A)) +
              HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.r : A))
                ((φ : (a : R) → A) W.a₂ : A) -
            HMul.hMul (β := A)
              (HAdd.hAdd (α := A) ((φ : (a : R) → A) C.t : A)
                (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C.s : A)))
              ((φ : (a : R) → A) W.a₁ : A) +
          3 * HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 2 -
        HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.s : A))
          ((φ : (a : R) → A) C.t : A)) =
    HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C.u⁻¹ : R) : A) 4 *
      (HSub.hSub (α := A) ((φ : (a : R) → A) W.a₄ : A)
                (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.s : A) ((φ : (a : R) → A) W.a₃ : A)) +
              HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.r : A))
                ((φ : (a : R) → A) W.a₂ : A) -
            HMul.hMul (β := A)
              (HAdd.hAdd (α := A) ((φ : (a : R) → A) C.t : A)
                (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C.s : A)))
              ((φ : (a : R) → A) W.a₁ : A) +
          3 * HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 2 -
        HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.s : A))
          ((φ : (a : R) → A) C.t : A))

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

Premises used: Units.coe_map_inv, MonoidHom.coe_coe
-- 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
⊢ HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A) 6 *
      (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₆ : A)
                  (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) W.a₄ : A)) +
                HMul.hMul (β := A) (HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 2)
                  ((φ : (a : R) → A) W.a₂ : A) +
              HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 3 -
            HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.t : A) ((φ : (a : R) → A) W.a₃ : A) -
          HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.t : A) 2 -
        HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C.t : A))
          ((φ : (a : R) → A) W.a₁ : A)) =
    HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) (↑C.u⁻¹ : R) : A) 6 *
      (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₆ : A)
                  (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) W.a₄ : A)) +
                HMul.hMul (β := A) (HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 2)
                  ((φ : (a : R) → A) W.a₂ : A) +
              HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 3 -
            HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.t : A) ((φ : (a : R) → A) W.a₃ : A) -
          HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.t : A) 2 -
        HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C.t : A))
          ((φ : (a : R) → A) W.a₁ : A))

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

Premises used: Units.coe_map_inv, MonoidHom.coe_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
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
⊢ 4 * W.b₈ = W.b₂ * W.b₆ - HPow.hPow (β := ℕ) W.b₄ 2

Tactic:
simp only [b₂, b₄, b₆, b₈]

Premises used: WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.b₈, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
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
⊢ 1728 * W.Δ = HPow.hPow (β := ℕ) W.c₄ 3 - HPow.hPow (β := ℕ) W.c₆ 2

Tactic:
simp only [b₂, b₄, b₆, b₈, c₄, c₆, Δ]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.c₄, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.b₈, WeierstrassCurve.c₆, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
rw : HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ = HPow.hPow (β := ℕ) W.a₁ 2
⊢ W.b₂ = HPow.hPow (β := ℕ) W.a₁ 2

Tactic:
rw [b₂]

Premises used: WeierstrassCurve.b₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ = HPow.hPow (β := ℕ) W.a₁ 2

Tactic:
linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₂, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
rw : 2 * W.a₄ + W.a₁ * W.a₃ = W.a₁ * W.a₃
⊢ W.b₄ = W.a₁ * W.a₃

Tactic:
rw [b₄]

Premises used: WeierstrassCurve.b₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = W.a₁ * W.a₃

Tactic:
linear_combination W.a₄ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₄, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
rw : HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆ = HPow.hPow (β := ℕ) W.a₃ 2
⊢ W.b₆ = HPow.hPow (β := ℕ) W.a₃ 2

Tactic:
rw [b₆]

Premises used: WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆ = HPow.hPow (β := ℕ) W.a₃ 2

Tactic:
linear_combination 2 * W.a₆ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
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
⊢ 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

Tactic:
rw [b₈]

Premises used: WeierstrassCurve.b₈
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 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 =
    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:
linear_combination (2 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ - W.a₄ ^ 2) * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, WeierstrassCurve.a₂, WeierstrassCurve.a₃, HPow.hPow, WeierstrassCurve.a₆, WeierstrassCurve.a₄, OfNat.ofNat, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
rw : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2) 2 - 24 * W.b₄ = HPow.hPow (β := ℕ) W.a₁ 4
⊢ W.c₄ = HPow.hPow (β := ℕ) W.a₁ 4

Tactic:
rw [c₄, b₂_of_char_two]

Premises used: WeierstrassCurve.b₂_of_char_two, WeierstrassCurve.c₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2) 2 - 24 * W.b₄ = HPow.hPow (β := ℕ) W.a₁ 4

Tactic:
linear_combination -12 * W.b₄ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.b₄, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
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
⊢ W.c₆ = HPow.hPow (β := ℕ) W.a₁ 6

Tactic:
rw [c₆, b₂_of_char_two]

Premises used: WeierstrassCurve.b₂_of_char_two, WeierstrassCurve.c₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ -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:
linear_combination (18 * W.a₁ ^ 2 * W.b₄ - 108 * W.b₆ - W.a₁ ^ 6) * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, WeierstrassCurve.b₄, HPow.hPow, OfNat.ofNat, WeierstrassCurve.a₁, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
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
⊢ W.Δ =
    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]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₂_of_char_two, WeierstrassCurve.b₄_of_char_two, WeierstrassCurve.b₆_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ -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:
linear_combination (-W.a₁ ^ 4 * W.b₈ - 14 * W.a₃ ^ 4) * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, WeierstrassCurve.a₃, WeierstrassCurve.b₈, HPow.hPow, OfNat.ofNat, Neg.neg, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ W.b₂ * W.b₆ = HPow.hPow (β := ℕ) W.b₄ 2

Tactic:
linear_combination -W.b_relation + 2 * W.b₈ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.b₈, WeierstrassCurve.b_relation, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ HPow.hPow (β := ℕ) W.c₄ 3 = HPow.hPow (β := ℕ) W.c₆ 2

Tactic:
linear_combination -W.c_relation + 864 * W.Δ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.Δ, WeierstrassCurve.c_relation, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
rw : HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ = HPow.hPow (β := ℕ) W.a₁ 2 + W.a₂
⊢ W.b₂ = HPow.hPow (β := ℕ) W.a₁ 2 + W.a₂

Tactic:
rw [b₂]

Premises used: WeierstrassCurve.b₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ = HPow.hPow (β := ℕ) W.a₁ 2 + W.a₂

Tactic:
linear_combination W.a₂ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₂, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
rw : 2 * W.a₄ + W.a₁ * W.a₃ = -W.a₄ + W.a₁ * W.a₃
⊢ W.b₄ = -W.a₄ + W.a₁ * W.a₃

Tactic:
rw [b₄]

Premises used: WeierstrassCurve.b₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = -W.a₄ + W.a₁ * W.a₃

Tactic:
linear_combination W.a₄ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₄, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
rw : HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆ = HPow.hPow (β := ℕ) W.a₃ 2 + W.a₆
⊢ W.b₆ = HPow.hPow (β := ℕ) W.a₃ 2 + W.a₆

Tactic:
rw [b₆]

Premises used: WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆ = HPow.hPow (β := ℕ) W.a₃ 2 + W.a₆

Tactic:
linear_combination W.a₆ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
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
⊢ 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

Tactic:
rw [b₈]

Premises used: WeierstrassCurve.b₈
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ 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:
linear_combination W.a₂ * W.a₆ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₂, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
rw : HPow.hPow (β := ℕ) W.b₂ 2 - 24 * W.b₄ = HPow.hPow (β := ℕ) W.b₂ 2
⊢ W.c₄ = HPow.hPow (β := ℕ) W.b₂ 2

Tactic:
rw [c₄]

Premises used: WeierstrassCurve.c₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ HPow.hPow (β := ℕ) W.b₂ 2 - 24 * W.b₄ = HPow.hPow (β := ℕ) W.b₂ 2

Tactic:
linear_combination -8 * W.b₄ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.b₄, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
rw : -HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆ = -HPow.hPow (β := ℕ) W.b₂ 3
⊢ W.c₆ = -HPow.hPow (β := ℕ) W.b₂ 3

Tactic:
rw [c₆]

Premises used: WeierstrassCurve.c₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ -HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆ = -HPow.hPow (β := ℕ) W.b₂ 3

Tactic:
linear_combination (12 * W.b₂ * W.b₄ - 72 * W.b₆) * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, WeierstrassCurve.b₂, WeierstrassCurve.b₄, OfNat.ofNat, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
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
⊢ W.Δ = -HPow.hPow (β := ℕ) W.b₂ 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) W.b₄ 3

Tactic:
rw [Δ]

Premises used: WeierstrassCurve.Δ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ -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:
linear_combination (-9 * W.b₆ ^ 2 + 3 * W.b₂ * W.b₄ * W.b₆) * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, HMul.hMul, WeierstrassCurve.b₂, WeierstrassCurve.b₄, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Neg.neg, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ W.b₈ = W.b₂ * W.b₆ - HPow.hPow (β := ℕ) W.b₄ 2

Tactic:
linear_combination W.b_relation - W.b₈ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.b₈, WeierstrassCurve.b_relation, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ HPow.hPow (β := ℕ) W.c₄ 3 = HPow.hPow (β := ℕ) W.c₆ 2

Tactic:
linear_combination -W.c_relation + 576 * W.Δ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.Δ, WeierstrassCurve.c_relation, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
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₂)
⊢ (W.map f).b₂ = (f : (a : R) → A) W.b₂

Tactic:
simp only [b₂, map_a₁, map_a₂]

Premises used: WeierstrassCurve.map_a₂, WeierstrassCurve.b₂, WeierstrassCurve.map_a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ 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:
map_simp