awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
a₁ : x.a₁ = x_1.a₁
⊢ x = x_1
have a₂ : x.a₂ = x_1.a₂
Tactic: ext
-- 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)
a₁ : x.a₁ = x_1.a₁
a₂ : x.a₂ = x_1.a₂
⊢ x = x_1
have a₃ : x.a₃ = x_1.a₃
Tactic: ext
-- 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)
a₁ : x.a₁ = x_1.a₁
a₂ : x.a₂ = x_1.a₂
a₃ : x.a₃ = x_1.a₃
⊢ x = x_1
have a₄ : x.a₄ = x_1.a₄
Tactic: ext
-- 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)
a₁ : x.a₁ = x_1.a₁
a₂ : x.a₂ = x_1.a₂
a₃ : x.a₃ = x_1.a₃
a₄ : x.a₄ = x_1.a₄
⊢ x = x_1
have a₆ : x.a₆ = x_1.a₆
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ W.twoTorsionPolynomial.discr = 16 * W.Δ
have simp : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 2 * HPow.hPow (β := ℕ) (2 * (2 * W.a₄ + W.a₁ * W.a₃)) 2 -
          HMul.hMul (α := R) 4 4 * HPow.hPow (β := ℕ) (2 * (2 * W.a₄ + W.a₁ * W.a₃)) 3 -
        4 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 3 * (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) -
      27 * HPow.hPow (α := R) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) 2 +
    HMul.hMul (α := R) 18 4 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) *
      (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) =
  16 *
    (-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₆))
Tactic: simp only [b₂, b₄, b₆, b₈, Δ, twoTorsionPolynomial, Cubic.discr]
-- 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
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }
have a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a
Tactic: ext
-- 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
a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }
have b : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.b = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.b
Tactic: ext
-- 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
a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a
b : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.b = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.b
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }
have c : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.c = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.c
Tactic: ext
-- 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
a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a
b : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.b = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.b
c : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.c = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.c
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }
have d : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.d = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.d
Tactic: ext
-- 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
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a
have a : Eq.{u + 1} (α := R) 4 0
Tactic: dsimp
-- 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
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.c = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.c
have c : 2 * W.b₄ = 0
Tactic: dsimp
-- 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
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }
have a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a
Tactic: ext
-- 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
a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }
have b : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.b = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.b
Tactic: ext
-- 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
a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a
b : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.b = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.b
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }
have c : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.c = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.c
Tactic: ext
-- 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
a : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a
b : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.b = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.b
c : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.c = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.c
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }
have d : { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.d = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.d
Tactic: ext
-- 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
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a
have a : Eq.{u + 1} (α := R) 4 1
Tactic: dsimp
-- 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
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R }.c = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.c
have c : 2 * W.b₄ = -W.b₄
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
hu : IsUnit.{u} (M := R) 2
⊢ IsUnit W.twoTorsionPolynomial.discr ↔ IsUnit W.Δ
have rw : IsUnit (HPow.hPow (α := R) (β := ℕ) 2 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ
Tactic: rw [twoTorsionPolynomial_discr, IsUnit.mul_iff, show (16 : R) = 2 ^ 4 by norm_num1]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.c₄ 3 = 0
have rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = 0 ↔ HPow.hPow (β := ℕ) W.c₄ 3 = 0
Tactic: rw [j, Units.mul_right_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = 0 ↔ HPow.hPow (β := ℕ) W.c₄ 3 = 0
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.c₄ 3 = 0
have rw₁ : HPow.hPow (β := ℕ) W.c₄ 3 = 0 ↔ HPow.hPow (β := ℕ) W.c₄ 3 = 0
Tactic: rw [j, Units.mul_right_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
h : W.c₄ = 0
⊢ W.j = 0
have rw : HPow.hPow (β := ℕ) W.c₄ 3 = 0
Tactic: rw [j_eq_zero_iff', h, zero_pow three_ne_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
h : W.c₄ = 0
rw : HPow.hPow (β := ℕ) W.c₄ 3 = 0
⊢ W.j = 0
have rw₁ : HPow.hPow (α := R) (β := ℕ) 0 3 = 0
Tactic: rw [j_eq_zero_iff', h, zero_pow three_ne_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
h : W.c₄ = 0
rw : HPow.hPow (β := ℕ) W.c₄ 3 = 0
rw₁ : HPow.hPow (α := R) (β := ℕ) 0 3 = 0
⊢ W.j = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [j_eq_zero_iff', h, zero_pow three_ne_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : IsReduced R
⊢ W.j = 0 ↔ W.c₄ = 0
have rw : HPow.hPow (β := ℕ) W.c₄ 3 = 0 ↔ W.c₄ = 0
Tactic: rw [j_eq_zero_iff', pow_eq_zero_iff three_ne_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : IsReduced R
rw : HPow.hPow (β := ℕ) W.c₄ 3 = 0 ↔ W.c₄ = 0
⊢ W.j = 0 ↔ W.c₄ = 0
have rw₁ : W.c₄ = 0 ↔ W.c₄ = 0
Tactic: rw [j_eq_zero_iff', pow_eq_zero_iff three_ne_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
have rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
Tactic: rw [j, W.c₄_of_char_two, ← pow_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
have rw₁ : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 4) 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
Tactic: rw [j, W.c₄_of_char_two, ← pow_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
rw₁ : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 4) 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
have rw₂ : (↑W.Δ'⁻¹ : R) * W.a₁ ^ HMul.hMul (α := ℕ) 4 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
Tactic: rw [j, W.c₄_of_char_two, ← pow_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.a₁ 12 = 0
have rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12 = 0 ↔ HPow.hPow (β := ℕ) W.a₁ 12 = 0
Tactic: rw [j_of_char_two, Units.mul_right_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12 = 0 ↔ HPow.hPow (β := ℕ) W.a₁ 12 = 0
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.a₁ 12 = 0
have rw₁ : HPow.hPow (β := ℕ) W.a₁ 12 = 0 ↔ HPow.hPow (β := ℕ) W.a₁ 12 = 0
Tactic: rw [j_of_char_two, Units.mul_right_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
h : W.a₁ = 0
⊢ W.j = 0
have rw : HPow.hPow (β := ℕ) W.a₁ 12 = 0
Tactic: rw [j_eq_zero_iff_of_char_two', h, zero_pow (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
h : W.a₁ = 0
rw : HPow.hPow (β := ℕ) W.a₁ 12 = 0
⊢ W.j = 0
have rw₁ : HPow.hPow (α := R) (β := ℕ) 0 12 = 0
Tactic: rw [j_eq_zero_iff_of_char_two', h, zero_pow (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
h : W.a₁ = 0
rw : HPow.hPow (β := ℕ) W.a₁ 12 = 0
rw₁ : HPow.hPow (α := R) (β := ℕ) 0 12 = 0
⊢ W.j = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [j_eq_zero_iff_of_char_two', h, zero_pow (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
inst_3 : IsReduced R
⊢ W.j = 0 ↔ W.a₁ = 0
have rw : HPow.hPow (β := ℕ) W.a₁ 12 = 0 ↔ W.a₁ = 0
Tactic: rw [j_eq_zero_iff_of_char_two', pow_eq_zero_iff (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 2
inst_3 : IsReduced R
rw : HPow.hPow (β := ℕ) W.a₁ 12 = 0 ↔ W.a₁ = 0
⊢ W.j = 0 ↔ W.a₁ = 0
have rw₁ : W.a₁ = 0 ↔ W.a₁ = 0
Tactic: rw [j_eq_zero_iff_of_char_two', pow_eq_zero_iff (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
have rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
Tactic: rw [j, W.c₄_of_char_three, ← pow_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
have rw₁ : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.b₂ 2) 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
Tactic: rw [j, W.c₄_of_char_three, ← pow_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
rw₁ : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.b₂ 2) 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
have rw₂ : (↑W.Δ'⁻¹ : R) * W.b₂ ^ HMul.hMul (α := ℕ) 2 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
Tactic: rw [j, W.c₄_of_char_three, ← pow_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.b₂ 6 = 0
have rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6 = 0 ↔ HPow.hPow (β := ℕ) W.b₂ 6 = 0
Tactic: rw [j_of_char_three, Units.mul_right_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
rw : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6 = 0 ↔ HPow.hPow (β := ℕ) W.b₂ 6 = 0
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.b₂ 6 = 0
have rw₁ : HPow.hPow (β := ℕ) W.b₂ 6 = 0 ↔ HPow.hPow (β := ℕ) W.b₂ 6 = 0
Tactic: rw [j_of_char_three, Units.mul_right_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
h : W.b₂ = 0
⊢ W.j = 0
have rw : HPow.hPow (β := ℕ) W.b₂ 6 = 0
Tactic: rw [j_eq_zero_iff_of_char_three', h, zero_pow (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
h : W.b₂ = 0
rw : HPow.hPow (β := ℕ) W.b₂ 6 = 0
⊢ W.j = 0
have rw₁ : HPow.hPow (α := R) (β := ℕ) 0 6 = 0
Tactic: rw [j_eq_zero_iff_of_char_three', h, zero_pow (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
h : W.b₂ = 0
rw : HPow.hPow (β := ℕ) W.b₂ 6 = 0
rw₁ : HPow.hPow (α := R) (β := ℕ) 0 6 = 0
⊢ W.j = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [j_eq_zero_iff_of_char_three', h, zero_pow (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
inst_3 : IsReduced R
⊢ W.j = 0 ↔ W.b₂ = 0
have rw : HPow.hPow (β := ℕ) W.b₂ 6 = 0 ↔ W.b₂ = 0
Tactic: rw [j_eq_zero_iff_of_char_three', pow_eq_zero_iff (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : CharP R 3
inst_3 : IsReduced R
rw : HPow.hPow (β := ℕ) W.b₂ 6 = 0 ↔ W.b₂ = 0
⊢ W.j = 0 ↔ W.b₂ = 0
have rw₁ : W.b₂ = 0 ↔ W.b₂ = 0
Tactic: rw [j_eq_zero_iff_of_char_three', pow_eq_zero_iff (Nat.succ_ne_zero _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
⊢ (↑(W.map f).Δ' : A) = (f : (a : R) → A) (↑W.Δ' : R)
have rw : (W.map f).Δ = (f : (a : R) → A) (↑W.Δ' : R)
Tactic: rw [coe_Δ', map_Δ, coe_Δ']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
rw : (W.map f).Δ = (f : (a : R) → A) (↑W.Δ' : R)
⊢ (↑(W.map f).Δ' : A) = (f : (a : R) → A) (↑W.Δ' : R)
have rw₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) W.Δ : A) ((f : (a : R) → A) (↑W.Δ' : R) : A)
Tactic: rw [coe_Δ', map_Δ, coe_Δ']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
rw : (W.map f).Δ = (f : (a : R) → A) (↑W.Δ' : R)
rw₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) W.Δ : A) ((f : (a : R) → A) (↑W.Δ' : R) : A)
⊢ (↑(W.map f).Δ' : A) = (f : (a : R) → A) (↑W.Δ' : R)
have rw₂ : Eq.{v + 1} (α := A) ((f : (a : R) → A) W.Δ : A) ((f : (a : R) → A) W.Δ : A)
Tactic: rw [coe_Δ', map_Δ, coe_Δ']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
⊢ Eq (α := Aˣ) (W.map f).Δ' (((Units.map (↑f : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) W.Δ')
have huv : (↑(W.map f).Δ' : A) = (↑(((Units.map (↑f : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) W.Δ') : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
⊢ (W.map f).j = (f : (a : R) → A) W.j
have rw : (↑(W.map f).Δ'⁻¹ : A) * HPow.hPow (β := ℕ) (W.map f).c₄ 3 = (f : (a : R) → A) W.j
Tactic: rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
rw : (↑(W.map f).Δ'⁻¹ : A) * HPow.hPow (β := ℕ) (W.map f).c₄ 3 = (f : (a : R) → A) W.j
⊢ (W.map f).j = (f : (a : R) → A) W.j
have rw₁ : HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (β := ℕ) (W.map f).c₄ 3) = (f : (a : R) → A) W.j
Tactic: rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]