awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
⊢ W.c₆ = 0
have rw : -864 * W.a₆ = 0
Tactic: rw [c₆_of_isShortNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
⊢ W.Δ = -HPow.hPow (β := ℕ) W.a₄ 3
have rw : -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) = -HPow.hPow (β := ℕ) W.a₄ 3
Tactic: rw [Δ_of_isShortNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
⊢ W.j = 6912 * HPow.hPow (β := ℕ) W.a₄ 3 / (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)
have h : (↑W.Δ' : F) ≠ 0
Tactic: have h := W.Δ'.ne_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
h : (↑W.Δ' : F) ≠ 0
⊢ W.j = 6912 * HPow.hPow (β := ℕ) W.a₄ 3 / (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)
have h₁ : -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) ≠ 0
Tactic: rw [coe_Δ', Δ_of_isShortNF] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
h : -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) ≠ 0
⊢ W.j = 6912 * HPow.hPow (β := ℕ) W.a₄ 3 / (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)
have rw : HPow.hPow (β := ℕ) (-48 * W.a₄) 3 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) =
  6912 * HPow.hPow (β := ℕ) W.a₄ 3 * (-16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2))
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isShortNF, Δ_of_isShortNF, div_eq_div_iff h (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
inst_3 : CharP F 3
⊢ W.j = 0
have rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (α := F) (β := ℕ) 0 3 = 0
Tactic: rw [j, c₄_of_isShortNF_of_char_three]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNF W).IsShortNF
have rw : (HSMul.hSMul (α := VariableChange R)
    { u := 1,
      r :=
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
          -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
      s := 0, t := 0 : VariableChange R }
    (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).IsShortNF
Tactic: rw [toShortNF, mul_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
⊢ (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).IsShortNF
have a₁ : (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₁ =
  0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
a₁ :
  (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₁ =
    0
⊢ (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).IsShortNF
have a₂ : (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₂ =
  0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
a₁ :
  (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₁ =
    0
a₂ :
  (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₂ =
    0
⊢ (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).IsShortNF
have a₃ : (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₃ =
  0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ W.b₂ = W.a₂
have rw : 4 * W.a₂ = W.a₂
Tactic: rw [b₂_of_isCharThreeJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ W.b₆ = W.a₆
have rw : 4 * W.a₆ = W.a₆
Tactic: rw [b₆_of_isCharThreeJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ W.b₈ = W.a₂ * W.a₆
have rw : 4 * W.a₂ * W.a₆ = W.a₂ * W.a₆
Tactic: rw [b₈_of_isCharThreeJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ W.c₄ = HPow.hPow (β := ℕ) W.a₂ 2
have rw : 16 * HPow.hPow (β := ℕ) W.a₂ 2 = HPow.hPow (β := ℕ) W.a₂ 2
Tactic: rw [c₄_of_isCharThreeJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ W.c₆ = -HPow.hPow (β := ℕ) W.a₂ 3
have rw : -64 * HPow.hPow (β := ℕ) W.a₂ 3 - 864 * W.a₆ = -HPow.hPow (β := ℕ) W.a₂ 3
Tactic: rw [c₆_of_isCharThreeJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ W.Δ = -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆
have rw : -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ - 432 * HPow.hPow (β := ℕ) W.a₆ 2 = -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆
Tactic: rw [Δ_of_isCharThreeJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
⊢ W.j = -HPow.hPow (β := ℕ) W.a₂ 3 / W.a₆
have h : (↑W.Δ' : F) ≠ 0
Tactic: have h := W.Δ'.ne_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : (↑W.Δ' : F) ≠ 0
⊢ W.j = -HPow.hPow (β := ℕ) W.a₂ 3 / W.a₆
have h₁ : -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0
Tactic: rw [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0
⊢ W.j = -HPow.hPow (β := ℕ) W.a₂ 3 / W.a₆
have rw : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₂ 2) 3 * W.a₆ =
  -HPow.hPow (β := ℕ) W.a₂ 3 * (-HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆)
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharThreeJNeZeroNF_of_char_three, Δ_of_isCharThreeJNeZeroNF_of_char_three,
    div_eq_div_iff h (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
⊢ W.j ≠ 0
have rw : -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
Tactic: rw [j_of_isCharThreeJNeZeroNF_of_char_three, div_ne_zero_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
⊢ -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
have h : (↑W.Δ' : F) ≠ 0
Tactic: have h := W.Δ'.ne_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : (↑W.Δ' : F) ≠ 0
⊢ -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
have rwa : ∀ (h : W.Δ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
Tactic: rwa [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : (↑W.Δ' : F) ≠ 0
rwa : ∀ (h : W.Δ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
⊢ -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
have rwa₁ : ∀ (h : -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
Tactic: rwa [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : (↑W.Δ' : F) ≠ 0
rwa : ∀ (h : W.Δ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
rwa₁ : ∀ (h : -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
⊢ -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
have rwa₂ : ∀ (h : -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
Tactic: rwa [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : W.IsCharThreeNF
⊢ W.IsCharNeTwoNF
have of_j_ne_zero : ∀ [W.IsCharThreeJNeZeroNF], W.IsCharNeTwoNF
Tactic: cases ‹W.IsCharThreeNF›
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : W.IsCharThreeNF
of_j_ne_zero : ∀ [W.IsCharThreeJNeZeroNF], W.IsCharNeTwoNF
⊢ W.IsCharNeTwoNF
have of_j_eq_zero : ∀ [W.IsShortNF], W.IsCharNeTwoNF
Tactic: cases ‹W.IsCharThreeNF›
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNFOfCharThree W).a₂ = W.b₂
have simp_rw : HPow.hPow (α := R) (β := ℕ) 1 2 *
    (W.a₂ - 2 * -W.a₁ * W.a₁ + HMul.hMul (α := R) 3 0 - HPow.hPow (β := ℕ) (2 * -W.a₁) 2) =
  HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂
Tactic: simp_rw [toShortNFOfCharThree, toCharNeTwoNF, variableChange_a₂, inv_one, Units.val_one, b₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
hb₂ : W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNFOfCharThree W).IsShortNF
have h : HMul.hMul (α := R) 2 2 = 1
Tactic: have h : (2 : R) * 2 = 1 := by linear_combination CharP.cast_eq_zero R 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
hb₂ : W.b₂ = 0
h : HMul.hMul (α := R) 2 2 = 1
this : Invertible (α := R) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNFOfCharThree W).IsShortNF
have H : (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).IsCharNeTwoNF
Tactic: have H := W.toCharNeTwoNF_spec
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeJNeZeroNF
have h : HMul.hMul (α := F) 2 2 = 1
Tactic: have h : (2 : F) * 2 = 1 := by linear_combination CharP.cast_eq_zero F 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeJNeZeroNF
have rw : (HSMul.hSMul (α := VariableChange F)
    { u := 1,
      r :=
        (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).a₄ /
          (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).a₂,
      s := 0, t := 0 : VariableChange F }
    (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W)).IsCharThreeJNeZeroNF
Tactic: rw [toCharThreeNF, mul_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F }
      W').IsCharThreeJNeZeroNF
have this₁ : W'.IsCharNeTwoNF
Tactic: haveI : W'.IsCharNeTwoNF := W.toCharNeTwoNF_spec
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F }
      W').IsCharThreeJNeZeroNF
have a₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₁ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
a₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F }
      W').IsCharThreeJNeZeroNF
have a₃ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₃ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
a₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₁ = 0
a₃ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₃ = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F }
      W').IsCharThreeJNeZeroNF
have a₄ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₄ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₄ = 0
have ha₂ : W'.a₂ ≠ 0
Tactic: have ha₂ : W'.a₂ ≠ 0 := W.toShortNFOfCharThree_a₂ ▸ hb₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
ha₂ : W'.a₂ ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₄ = 0
have a₄ : W'.a₄ * (HPow.hPow (β := ℕ) W'.a₂ 2 * HAdd.hAdd (α := F) 1 2 + W'.a₄ * 3) = 0
Tactic: simp [field, variableChange_a₄, -mul_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsShortNF
have rw : (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).IsShortNF
Tactic: rw [toCharThreeNF, toShortNFOfCharThree_a₂, hb₂, div_zero, ← VariableChange.one_def, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
have pos : ∀ (hb₂ : W.b₂ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
Tactic: by_cases hb₂ : W.b₂ = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
pos : ∀ (hb₂ : W.b₂ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
have neg : ∀ (hb₂ : ¬W.b₂ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
Tactic: by_cases hb₂ : W.b₂ = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
have this : (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsShortNF
Tactic: haveI := W.toCharThreeNF_spec_of_b₂_eq_zero hb₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
hb₂ : ¬W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
have this : (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeJNeZeroNF
Tactic: haveI := W.toCharThreeNF_spec_of_b₂_ne_zero hb₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ W.b₂ = 1 + 4 * W.a₂
have rw : HPow.hPow (α := R) (β := ℕ) 1 2 + 4 * W.a₂ = 1 + 4 * W.a₂
Tactic: rw [b₂, a₁_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ W.b₄ = 0
have rw : HMul.hMul (α := R) 2 0 + W.a₁ * 0 = 0
Tactic: rw [b₄, a₃_of_isCharTwoJNeZeroNF, a₄_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ W.b₆ = 4 * W.a₆
have rw : HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₆ = 4 * W.a₆
Tactic: rw [b₆, a₃_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆
have rw : HPow.hPow (α := R) (β := ℕ) 1 2 * W.a₆ + 4 * W.a₂ * W.a₆ - HMul.hMul (α := R) 1 0 * 0 +
      W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
    HPow.hPow (α := R) (β := ℕ) 0 2 =
  W.a₆ + 4 * W.a₂ * W.a₆
Tactic: rw [b₈, a₁_of_isCharTwoJNeZeroNF, a₃_of_isCharTwoJNeZeroNF, a₄_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ W.c₄ = HPow.hPow (β := ℕ) W.b₂ 2
have rw : HPow.hPow (β := ℕ) W.b₂ 2 - HMul.hMul (α := R) 24 0 = HPow.hPow (β := ℕ) W.b₂ 2
Tactic: rw [c₄, b₄_of_isCharTwoJNeZeroNF]