awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
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₆))
⊢ W.twoTorsionPolynomial.discr = 16 * W.Δ

Tactic:
simp only [b₂, b₄, b₆, b₈, Δ, twoTorsionPolynomial, Cubic.discr]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.twoTorsionPolynomial, WeierstrassCurve.b₈, Cubic.discr, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
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
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ : Cubic R } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
a : Eq.{u + 1} (α := R) 4 0
⊢ { 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:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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 }.b = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.b

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
c : 2 * W.b₄ = 0
⊢ { 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:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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 }.d = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.d

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
⊢ Eq.{u + 1} (α := R) 4 0

Tactic:
linear_combination 2 * CharP.cast_eq_zero R 2

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

Tactic:
linear_combination 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
⊢ W.twoTorsionPolynomial.discr = 0

Tactic:
linear_combination W.twoTorsionPolynomial_discr + 8 * W.Δ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.Δ, OfNat.ofNat, WeierstrassCurve.twoTorsionPolynomial_discr
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
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
⊢ { 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₆ }

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
a : Eq.{u + 1} (α := R) 4 1
⊢ { 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:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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 }.b = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.b

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
c : 2 * W.b₄ = -W.b₄
⊢ { 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:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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 }.d = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.d

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ Eq.{u + 1} (α := R) 4 1

Tactic:
linear_combination CharP.cast_eq_zero R 3

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

Tactic:
linear_combination 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
⊢ W.twoTorsionPolynomial.discr = W.Δ

Tactic:
linear_combination W.twoTorsionPolynomial_discr + 5 * W.Δ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.Δ, OfNat.ofNat, WeierstrassCurve.twoTorsionPolynomial_discr
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
hu : IsUnit.{u} (M := R) 2
⊢ 16 = HPow.hPow (α := R) (β := ℕ) 2 4

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
hu : IsUnit.{u} (M := R) 2
rw : IsUnit (HPow.hPow (α := R) (β := ℕ) 2 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ
⊢ IsUnit W.twoTorsionPolynomial.discr ↔ IsUnit W.Δ

Tactic:
rw [twoTorsionPolynomial_discr, IsUnit.mul_iff, show (16 : R) = 2 ^ 4 by norm_num1]

Premises used: IsUnit.mul_iff, WeierstrassCurve.twoTorsionPolynomial_discr
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
hu : IsUnit.{u} (M := R) 2
⊢ IsUnit (HPow.hPow (α := R) (β := ℕ) 2 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ

Tactic:
and_iff_right <| hu.pow 4

Premises used: and_iff_right, IsUnit.pow, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
hu : IsUnit.{u} (M := R) 2
⊢ IsUnit (HPow.hPow (α := R) (β := ℕ) 2 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ

Tactic:
exact and_iff_right <| hu.pow 4

Premises used: and_iff_right, IsUnit.pow, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
hu : IsUnit.{u} (M := R) 2
hΔ : IsUnit W.Δ
⊢ W.twoTorsionPolynomial.discr ≠ 0

Tactic:
((W.twoTorsionPolynomial_discr_isUnit hu).mpr hΔ).ne_zero

Premises used: Iff.mpr, WeierstrassCurve.twoTorsionPolynomial_discr_isUnit, IsUnit.ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
⊢ IsUnit W.Δ

Tactic:
IsElliptic.isUnit

Premises used: WeierstrassCurve.IsElliptic.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
⊢ (↑W.Δ' : R) = W.Δ

Tactic:
rfl

Premises used: WeierstrassCurve.Δ, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₁ rw₂ : HPow.hPow (β := ℕ) W.c₄ 3 = 0 ↔ HPow.hPow (β := ℕ) W.c₄ 3 = 0
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.c₄ 3 = 0

Tactic:
rw [j, Units.mul_right_eq_zero]

Premises used: WeierstrassCurve.j, Units.mul_right_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ W.j = 0

Tactic:
rw [j_eq_zero_iff', h, zero_pow three_ne_zero]

Premises used: WeierstrassCurve.j_eq_zero_iff', three_ne_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₁ rw₂ : W.c₄ = 0 ↔ W.c₄ = 0
⊢ W.j = 0 ↔ W.c₄ = 0

Tactic:
rw [j_eq_zero_iff', pow_eq_zero_iff three_ne_zero]

Premises used: pow_eq_zero_iff, WeierstrassCurve.j_eq_zero_iff', three_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₂ rw₃ : (↑W.Δ'⁻¹ : R) * W.a₁ ^ HMul.hMul (α := ℕ) 4 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.a₁ 12

Tactic:
rw [j, W.c₄_of_char_two, ← pow_mul]

Premises used: WeierstrassCurve.j, pow_mul, WeierstrassCurve.c₄_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₁ rw₂ : HPow.hPow (β := ℕ) W.a₁ 12 = 0 ↔ HPow.hPow (β := ℕ) W.a₁ 12 = 0
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.a₁ 12 = 0

Tactic:
rw [j_of_char_two, Units.mul_right_eq_zero]

Premises used: WeierstrassCurve.j_of_char_two, Units.mul_right_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ W.j = 0

Tactic:
rw [j_eq_zero_iff_of_char_two', h, zero_pow (Nat.succ_ne_zero _)]

Premises used: Nat.succ_ne_zero, WeierstrassCurve.j_eq_zero_iff_of_char_two', zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₁ rw₂ : W.a₁ = 0 ↔ W.a₁ = 0
⊢ W.j = 0 ↔ W.a₁ = 0

Tactic:
rw [j_eq_zero_iff_of_char_two', pow_eq_zero_iff (Nat.succ_ne_zero _)]

Premises used: pow_eq_zero_iff, Nat.succ_ne_zero, WeierstrassCurve.j_eq_zero_iff_of_char_two'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₂ rw₃ : (↑W.Δ'⁻¹ : R) * W.b₂ ^ HMul.hMul (α := ℕ) 2 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6
⊢ W.j = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.b₂ 6

Tactic:
rw [j, W.c₄_of_char_three, ← pow_mul]

Premises used: WeierstrassCurve.c₄_of_char_three, WeierstrassCurve.j, pow_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₁ rw₂ : HPow.hPow (β := ℕ) W.b₂ 6 = 0 ↔ HPow.hPow (β := ℕ) W.b₂ 6 = 0
⊢ W.j = 0 ↔ HPow.hPow (β := ℕ) W.b₂ 6 = 0

Tactic:
rw [j_of_char_three, Units.mul_right_eq_zero]

Premises used: WeierstrassCurve.j_of_char_three, Units.mul_right_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ W.j = 0

Tactic:
rw [j_eq_zero_iff_of_char_three', h, zero_pow (Nat.succ_ne_zero _)]

Premises used: Nat.succ_ne_zero, WeierstrassCurve.j_eq_zero_iff_of_char_three', zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₁ rw₂ : W.b₂ = 0 ↔ W.b₂ = 0
⊢ W.j = 0 ↔ W.b₂ = 0

Tactic:
rw [j_eq_zero_iff_of_char_three', pow_eq_zero_iff (Nat.succ_ne_zero _)]

Premises used: pow_eq_zero_iff, Nat.succ_ne_zero, WeierstrassCurve.j_eq_zero_iff_of_char_three'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
inst_2 : Nontrivial R
hu : IsUnit.{u} (M := R) 2
⊢ W.twoTorsionPolynomial.discr ≠ 0

Tactic:
W.twoTorsionPolynomial_discr_ne_zero hu W.isUnit_Δ

Premises used: WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero, WeierstrassCurve.isUnit_Δ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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).IsElliptic

Tactic:
simp only [isElliptic_iff, map_Δ, W.isUnit_Δ.map]

Premises used: WeierstrassCurve.isUnit_Δ, IsUnit.map, WeierstrassCurve.isElliptic_iff, WeierstrassCurve.map_Δ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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)
rw₂ rw₃ : Eq.{v + 1} (α := A) ((f : (a : R) → A) W.Δ : A) ((f : (a : R) → A) W.Δ : A)
⊢ (↑(W.map f).Δ' : A) = (f : (a : R) → A) (↑W.Δ' : R)

Tactic:
rw [coe_Δ', map_Δ, coe_Δ']

Premises used: WeierstrassCurve.coe_Δ', WeierstrassCurve.map_Δ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
huv : (↑(W.map f).Δ' : A) = (↑(((Units.map (↑f : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) W.Δ') : A)
⊢ Eq (α := Aˣ) (W.map f).Δ' (((Units.map (↑f : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) W.Δ')

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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) = (↑(((Units.map (↑f : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) W.Δ') : A)

Tactic:
W.coe_map_Δ' f

Premises used: WeierstrassCurve.coe_map_Δ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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) = (↑(((Units.map (↑f : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) W.Δ') : A)

Tactic:
exact W.coe_map_Δ' f

Premises used: WeierstrassCurve.coe_map_Δ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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.Δ'⁻¹)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
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
rw₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (β := ℕ) (W.map f).c₄ 3) = (f : (a : R) → A) W.j
rw₂ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    (f : (a : R) → A) W.j
rw₃ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    (f : (a : R) → A) ((↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3)
rw₄ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      ((f : (a : R) → A) (HPow.hPow (β := ℕ) W.c₄ 3) : A)
rw₅ rw₆ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3)
⊢ (W.map f).j = (f : (a : R) → A) W.j

Tactic:
rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]

Premises used: WeierstrassCurve.j, map_pow, map_mul, WeierstrassCurve.coe_inv_map_Δ', WeierstrassCurve.map_c₄
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
y : ↥Y
x : ↥(fiber f y)
⊢ Eq (α := ↥(Spec (Y.residueField y))) ((fiberToSpecResidueField f y) x : ↥(Spec (Y.residueField y)))
    (IsLocalRing.closedPoint (↑(Y.residueField y) : Type u) : PrimeSpectrum (↑(Y.residueField y) : Type u))

Tactic:
Subsingleton.elim (α := PrimeSpectrum _) _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X_1 Y_1 P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ Y.fromSpecResidueField y ≫ g = Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y))
    (Spec.map (Scheme.Hom.residueFieldMap g y))

Tactic:
.of_right (h₁₂ := pullback.fst _ _) ?_ ?_
      (IsPullback.of_hasPullback f (Z.fromSpecResidueField (g y)))

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.fromSpecResidueField, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.IsPullback.of_right, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
refine_1 :
  IsPullback
    (CategoryStruct.comp (Y := pullback (Y := Spec (Z.residueField (g y))) f (Z.fromSpecResidueField (g y)))
      (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
      (pullback.fst f (Z.fromSpecResidueField (g y))))
    (Scheme.Hom.fiberToSpecResidueField snd y) f
    (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))
refine_2 :
  pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField f (g y) =
    Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y))
    (Spec.map (Scheme.Hom.residueFieldMap g y))

Tactic:
refine .of_right (h₁₂ := pullback.fst _ _) ?_ ?_
      (IsPullback.of_hasPullback f (Z.fromSpecResidueField (g y)))
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (CategoryStruct.comp (Y := pullback (Y := Spec (Z.residueField (g y))) f (Z.fromSpecResidueField (g y)))
      (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
      (pullback.fst f (Z.fromSpecResidueField (g y))))
    (Scheme.Hom.fiberToSpecResidueField snd y) f
    (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))

Tactic:
simpa using (IsPullback.of_hasPullback _ _).paste_horiz h

Premises used: CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField f (g y) =
    Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)

Tactic:
simp [Scheme.Hom.fiberToSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField