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.IsCharTwoJNeZeroNF
⊢ W.c₆ = -HPow.hPow (β := ℕ) W.b₂ 3 - 864 * W.a₆
have rw : -HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * 0 - 216 * (4 * W.a₆) = -HPow.hPow (β := ℕ) W.b₂ 3 - 864 * W.a₆
Tactic: rw [c₆, b₄_of_isCharTwoJNeZeroNF, b₆_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
inst_2 : CharP R 2
⊢ W.b₂ = 1
have rw : 1 + 4 * W.a₂ = 1
Tactic: rw [b₂_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
inst_2 : CharP R 2
⊢ W.b₆ = 0
have rw : 4 * W.a₆ = 0
Tactic: rw [b₆_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
inst_2 : CharP R 2
⊢ W.b₈ = W.a₆
have rw : W.a₆ + 4 * W.a₂ * W.a₆ = W.a₆
Tactic: rw [b₈_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
inst_2 : CharP R 2
⊢ W.c₄ = 1
have rw : HPow.hPow (α := R) (β := ℕ) 1 2 = 1
Tactic: rw [c₄_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two]
-- 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
inst_2 : CharP R 2
⊢ W.c₆ = 1
have rw : -HPow.hPow (α := R) (β := ℕ) 1 3 - 864 * W.a₆ = 1
Tactic: rw [c₆_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two]
-- 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
inst_2 : CharP R 2
⊢ W.Δ = W.a₆
have rw : -HPow.hPow (α := R) (β := ℕ) 1 2 * W.a₆ - 8 * HPow.hPow (α := R) (β := ℕ) 0 3 - 27 * HPow.hPow (α := R) (β := ℕ) 0 2 +
    HMul.hMul (α := R) 9 1 * 0 * 0 =
  W.a₆
Tactic: rw [Δ, b₂_of_isCharTwoJNeZeroNF_of_char_two, b₄_of_isCharTwoJNeZeroNF,
    b₆_of_isCharTwoJNeZeroNF_of_char_two, b₈_of_isCharTwoJNeZeroNF_of_char_two]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
⊢ W.j = 1 / W.a₆
have rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
⊢ W.j = 1 / W.a₆
have rw₁ : (↑W.Δ' : F)⁻¹ * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₁ : (↑W.Δ' : F)⁻¹ * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
⊢ W.j = 1 / W.a₆
have rw₂ : HPow.hPow (β := ℕ) W.c₄ 3 / (↑W.Δ' : F) = 1 / W.a₆
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₁ : (↑W.Δ' : F)⁻¹ * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₂ : HPow.hPow (β := ℕ) W.c₄ 3 / (↑W.Δ' : F) = 1 / W.a₆
⊢ W.j = 1 / W.a₆
have rw₃ : HPow.hPow (β := ℕ) W.c₄ 3 / W.Δ = 1 / W.a₆
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₁ : (↑W.Δ' : F)⁻¹ * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₂ : HPow.hPow (β := ℕ) W.c₄ 3 / (↑W.Δ' : F) = 1 / W.a₆
rw₃ : HPow.hPow (β := ℕ) W.c₄ 3 / W.Δ = 1 / W.a₆
⊢ W.j = 1 / W.a₆
have rw₄ : HPow.hPow (α := F) (β := ℕ) 1 3 / W.Δ = 1 / W.a₆
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₁ : (↑W.Δ' : F)⁻¹ * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₂ : HPow.hPow (β := ℕ) W.c₄ 3 / (↑W.Δ' : F) = 1 / W.a₆
rw₃ : HPow.hPow (β := ℕ) W.c₄ 3 / W.Δ = 1 / W.a₆
rw₄ : HPow.hPow (α := F) (β := ℕ) 1 3 / W.Δ = 1 / W.a₆
⊢ W.j = 1 / W.a₆
have rw₅ : HPow.hPow (α := F) (β := ℕ) 1 3 / W.a₆ = 1 / W.a₆
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₁ : (↑W.Δ' : F)⁻¹ * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₂ : HPow.hPow (β := ℕ) W.c₄ 3 / (↑W.Δ' : F) = 1 / W.a₆
rw₃ : HPow.hPow (β := ℕ) W.c₄ 3 / W.Δ = 1 / W.a₆
rw₄ : HPow.hPow (α := F) (β := ℕ) 1 3 / W.Δ = 1 / W.a₆
rw₅ : HPow.hPow (α := F) (β := ℕ) 1 3 / W.a₆ = 1 / W.a₆
⊢ W.j = 1 / W.a₆
have rw₆ : 1 / W.a₆ = 1 / W.a₆
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]
-- 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
⊢ W.j ≠ 0
have rw : Ne.{u_2 + 1} (α := F) 1 0 ∧ W.a₆ ≠ 0
Tactic: rw [j_of_isCharTwoJNeZeroNF_of_char_two, 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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
⊢ Ne.{u_2 + 1} (α := F) 1 0 ∧ W.a₆ ≠ 0
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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
h : (↑W.Δ' : F) ≠ 0
⊢ Ne.{u_2 + 1} (α := F) 1 0 ∧ W.a₆ ≠ 0
have h₁ : W.a₆ ≠ 0
Tactic: rw [coe_Δ', Δ_of_isCharTwoJNeZeroNF_of_char_two] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ W.b₂ = 0
have rw : HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0 = 0
Tactic: rw [b₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ W.b₄ = 2 * W.a₄
have rw : 2 * W.a₄ + 0 * W.a₃ = 2 * W.a₄
Tactic: rw [b₄, a₁_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ W.b₈ = -HPow.hPow (β := ℕ) W.a₄ 2
have rw : HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₆ + HMul.hMul (α := R) 4 0 * W.a₆ - 0 * W.a₃ * W.a₄ +
      0 * HPow.hPow (β := ℕ) W.a₃ 2 -
    HPow.hPow (β := ℕ) W.a₄ 2 =
  -HPow.hPow (β := ℕ) W.a₄ 2
Tactic: rw [b₈, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ W.c₄ = -48 * W.a₄
have rw : HPow.hPow (α := R) (β := ℕ) 0 2 - 24 * (2 * W.a₄) = -48 * W.a₄
Tactic: rw [c₄, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ W.c₆ = -216 * W.b₆
have rw : -HPow.hPow (α := R) (β := ℕ) 0 3 + HMul.hMul (α := R) 36 0 * (2 * W.a₄) - 216 * W.b₆ = -216 * W.b₆
Tactic: rw [c₆, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ W.Δ = -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)
have rw : -HPow.hPow (α := R) (β := ℕ) 0 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) (2 * W.a₄) 3 - 27 * HPow.hPow (β := ℕ) W.b₆ 2 +
    HMul.hMul (α := R) 9 0 * (2 * W.a₄) * W.b₆ =
  -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)
Tactic: rw [Δ, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
⊢ W.b₄ = 0
have rw : 2 * W.a₄ = 0
Tactic: rw [b₄_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
⊢ W.b₈ = HPow.hPow (β := ℕ) W.a₄ 2
have rw : -HPow.hPow (β := ℕ) W.a₄ 2 = HPow.hPow (β := ℕ) W.a₄ 2
Tactic: rw [b₈_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
⊢ W.c₄ = 0
have rw : -48 * W.a₄ = 0
Tactic: rw [c₄_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
⊢ W.c₆ = 0
have rw : -216 * W.b₆ = 0
Tactic: rw [c₆_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
⊢ W.Δ = HPow.hPow (β := ℕ) W.a₃ 4
have rw : -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₃ 2) 2) = HPow.hPow (β := ℕ) W.a₃ 4
Tactic: rw [Δ_of_isCharTwoJEqZeroNF, b₆_of_char_two]
-- 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.IsCharTwoJEqZeroNF
⊢ W.j = 110592 * HPow.hPow (β := ℕ) W.a₄ 3 / (64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 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.IsCharTwoJEqZeroNF
h : (↑W.Δ' : F) ≠ 0
⊢ W.j = 110592 * HPow.hPow (β := ℕ) W.a₄ 3 / (64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)
have h₁ : -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) ≠ 0
Tactic: rw [coe_Δ', Δ_of_isCharTwoJEqZeroNF] 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.IsCharTwoJEqZeroNF
h : -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) ≠ 0
⊢ W.j = 110592 * HPow.hPow (β := ℕ) W.a₄ 3 / (64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)
have rw : HPow.hPow (β := ℕ) (-48 * W.a₄) 3 * (64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) =
  110592 * HPow.hPow (β := ℕ) W.a₄ 3 * -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)
Tactic: rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJEqZeroNF, Δ_of_isCharTwoJEqZeroNF, div_eq_div_iff h (neg_ne_zero.1 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.IsCharTwoJEqZeroNF
inst_3 : CharP F 2
⊢ W.j = 0
have rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (α := F) (β := ℕ) 0 3 = 0
Tactic: rw [j, c₄_of_isCharTwoJEqZeroNF_of_char_two]
-- 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 2
ha₁ : W.a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).IsCharTwoJEqZeroNF
have a₁ : (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF 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 : CharP R 2
ha₁ : W.a₁ = 0
a₁ : (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).IsCharTwoJEqZeroNF
have a₂ : (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF 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 : CharP R 2
ha₁ : W.a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).a₂ = 0
have a₂ : HPow.hPow (α := R) (β := ℕ) 1 2 * (W.a₂ - 0 * W.a₁ + 3 * W.a₂ - HPow.hPow (α := R) (β := ℕ) 0 2) = 0
Tactic: simp_rw [toCharTwoJEqZeroNF, variableChange_a₂, inv_one, Units.val_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF
have a₁ : (W.toCharTwoJNeZeroNF ha₁ • W).a₁ = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
a₁ : (W.toCharTwoJNeZeroNF ha₁ • W).a₁ = 1
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF
have a₃ : (W.toCharTwoJNeZeroNF ha₁ • 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 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
a₁ : (W.toCharTwoJNeZeroNF ha₁ • W).a₁ = 1
a₃ : (W.toCharTwoJNeZeroNF ha₁ • W).a₃ = 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF
have a₄ : (W.toCharTwoJNeZeroNF ha₁ • 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 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).a₃ = 0
have a₃ : HPow.hPow (β := ℕ) W.a₁ 3 * W.a₃ * HAdd.hAdd (α := F) 1 1 +
    2 * (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₄ + HPow.hPow (β := ℕ) W.a₃ 2) =
  0
Tactic: simp [field, toCharTwoJNeZeroNF, 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 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).a₄ = 0
have a₄ : W.a₁ * (W.a₁ * W.a₄ + 2 * W.a₃ * W.a₂) - (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₄ + HPow.hPow (β := ℕ) W.a₃ 2) +
    HPow.hPow (β := ℕ) W.a₃ 2 * 3 =
  0
Tactic: simp [field, toCharTwoJNeZeroNF, variableChange_a₄, -mul_eq_zero]
-- 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 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
have pos : ∀ (ha₁ : W.a₁ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
Tactic: by_cases ha₁ : W.a₁ = 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 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
pos : ∀ (ha₁ : W.a₁ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
have neg : ∀ (ha₁ : ¬W.a₁ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
Tactic: by_cases ha₁ : W.a₁ = 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 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : W.a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
have pos : (HSMul.hSMul (α := VariableChange F) W.toCharTwoJEqZeroNF W).IsCharTwoNF
Tactic: rw [toCharTwoNF, dif_pos ha₁]
-- 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 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : W.a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoJEqZeroNF W).IsCharTwoNF
have this : (HSMul.hSMul (α := VariableChange F) W.toCharTwoJEqZeroNF W).IsCharTwoJEqZeroNF
Tactic: haveI := W.toCharTwoJEqZeroNF_spec ha₁
-- 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 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : ¬W.a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
have neg : (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoNF
Tactic: rw [toCharTwoNF, dif_neg ha₁]
-- 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 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : ¬W.a₁ = 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoNF
have this : (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF
Tactic: haveI := W.toCharTwoJNeZeroNF_spec ha₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] = P
have h : ∀ (n : Fin (Nat.succ 0).succ.succ), ![P x, P y, P z] n = P n
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n
have h : ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
h :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![P x, P y, P z] n = P n
have h₁ : ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
h :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![P x, P y, P z] n = P n
have h₂ : ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f : (a : R) → S) ∘ (u • P) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
have h : ∀ («x» : Fin 3),
  ((⇑f : (a : R) → S) ∘ (u • P)) «x» =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) «x»
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u • P ≈ v • Q ↔ P ≈ Q
have rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
Tactic: rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
⊢ u • P ≈ v • Q ↔ P ≈ Q
have rw₁ : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
Tactic: rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
rw₁ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
⊢ u • P ≈ v • Q ↔ P ≈ Q
have rw₂ : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦v • Q⟧ ↔
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
Tactic: rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]