awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Ne.{u_2 + 1} (α := F) 2 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
neg :
  (if Eq.{u_2 + 1} (α := F) 1728 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 1728 1728 then ofJ1728 F else ofJNe0Or1728 1728) =
    ofJ1728 F
⊢ ofJ 1728 = ofJ1728 F
have neg₁ : (if HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 = 0 then
    if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
  else
    if
        HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 =
          HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 then
      ofJ1728 F
    else ofJNe0Or1728 (HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3)) =
  ofJ1728 F
Tactic: rw [ofJ, show (1728 : F) = 2 ^ 6 * 3 ^ 3 by norm_num1,
      if_neg (mul_ne_zero (pow_ne_zero 6 h2) (pow_ne_zero 3 h3)), if_pos rfl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Ne.{u_2 + 1} (α := F) 2 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
neg :
  (if Eq.{u_2 + 1} (α := F) 1728 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 1728 1728 then ofJ1728 F else ofJNe0Or1728 1728) =
    ofJ1728 F
neg₁ :
  (if HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 = 0 then
      if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else
      if
          HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 =
            HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 then
        ofJ1728 F
      else ofJNe0Or1728 (HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3)) =
    ofJ1728 F
⊢ ofJ 1728 = ofJ1728 F
have neg₂ : (if
      HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 =
        HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 then
    ofJ1728 F
  else ofJNe0Or1728 (HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3)) =
  ofJ1728 F
Tactic: rw [ofJ, show (1728 : F) = 2 ^ 6 * 3 ^ 3 by norm_num1,
      if_neg (mul_ne_zero (pow_ne_zero 6 h2) (pow_ne_zero 3 h3)), if_pos rfl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Ne.{u_2 + 1} (α := F) 2 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
neg :
  (if Eq.{u_2 + 1} (α := F) 1728 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 1728 1728 then ofJ1728 F else ofJNe0Or1728 1728) =
    ofJ1728 F
neg₁ :
  (if HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 = 0 then
      if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else
      if
          HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 =
            HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 then
        ofJ1728 F
      else ofJNe0Or1728 (HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3)) =
    ofJ1728 F
neg₂ :
  (if
        HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 =
          HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3 then
      ofJ1728 F
    else ofJNe0Or1728 (HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3)) =
    ofJ1728 F
⊢ ofJ 1728 = ofJ1728 F
have neg₃ : ofJ1728 F = ofJ1728 F
Tactic: rw [ofJ, show (1728 : F) = 2 ^ 6 * 3 ^ 3 by norm_num1,
      if_neg (mul_ne_zero (pow_ne_zero 6 h2) (pow_ne_zero 3 h3)), if_pos rfl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Eq.{u_2 + 1} (α := F) 2 0
⊢ ofJ 1728 = ofJ0 F
have rw : (if Eq.{u_2 + 1} (α := F) 1728 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
  else if Eq.{u_2 + 1} (α := F) 1728 1728 then ofJ1728 F else ofJNe0Or1728 1728) =
  ofJ0 F
Tactic: rw [ofJ, if_pos (by linear_combination 864 * h2),
    if_neg ((show (3 : F) = 1 by linear_combination h2) ▸ one_ne_zero)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Eq.{u_2 + 1} (α := F) 2 0
rw :
  (if Eq.{u_2 + 1} (α := F) 1728 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 1728 1728 then ofJ1728 F else ofJNe0Or1728 1728) =
    ofJ0 F
⊢ ofJ 1728 = ofJ0 F
have rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ0 F
Tactic: rw [ofJ, if_pos (by linear_combination 864 * h2),
    if_neg ((show (3 : F) = 1 by linear_combination h2) ▸ one_ne_zero)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Eq.{u_2 + 1} (α := F) 2 0
rw :
  (if Eq.{u_2 + 1} (α := F) 1728 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 1728 1728 then ofJ1728 F else ofJNe0Or1728 1728) =
    ofJ0 F
rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ0 F
⊢ ofJ 1728 = ofJ0 F
have rw₂ : ofJ0 F = ofJ0 F
Tactic: rw [ofJ, if_pos (by linear_combination 864 * h2),
    if_neg ((show (3 : F) = 1 by linear_combination h2) ▸ one_ne_zero)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
⊢ ofJ j = ofJNe0Or1728 j
have rw : (if j = 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
  else if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) =
  ofJNe0Or1728 j
Tactic: rw [ofJ, if_neg h0, if_neg h1728]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
rw :
  (if j = 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) =
    ofJNe0Or1728 j
⊢ ofJ j = ofJNe0Or1728 j
have rw₁ : (if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) = ofJNe0Or1728 j
Tactic: rw [ofJ, if_neg h0, if_neg h1728]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
rw :
  (if j = 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) =
    ofJNe0Or1728 j
rw₁ : (if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) = ofJNe0Or1728 j
⊢ ofJ j = ofJNe0Or1728 j
have rw₂ : ofJNe0Or1728 j = ofJNe0Or1728 j
Tactic: rw [ofJ, if_neg h0, if_neg h1728]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
⊢ (ofJ j).IsElliptic
have pos : ∀ (h0 : j = 0), (ofJ j).IsElliptic
Tactic: by_cases h0 : j = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
pos : ∀ (h0 : j = 0), (ofJ j).IsElliptic
⊢ (ofJ j).IsElliptic
have neg : ∀ (h0 : ¬j = 0), (ofJ j).IsElliptic
Tactic: by_cases h0 : j = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : j = 0
⊢ (ofJ j).IsElliptic
have pos : ∀ (h3 : Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).IsElliptic
Tactic: by_cases h3 : (3 : F) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : j = 0
pos : ∀ (h3 : Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).IsElliptic
⊢ (ofJ j).IsElliptic
have neg : ∀ (h3 : ¬Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).IsElliptic
Tactic: by_cases h3 : (3 : F) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : j = 0
h3 : Eq.{u_2 + 1} (α := F) 3 0
⊢ (ofJ j).IsElliptic
have this : Fact (IsUnit.{u_2} (M := F) 2)
Tactic: have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : j = 0
h3 : Eq.{u_2 + 1} (α := F) 3 0
this : Fact (IsUnit.{u_2} (M := F) 2)
⊢ (ofJ j).IsElliptic
have pos : (ofJ1728 F).IsElliptic
Tactic: rw [h0, ofJ_0_of_three_eq_zero h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : j = 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
⊢ (ofJ j).IsElliptic
have this : Fact (IsUnit.{u_2} (M := F) 3)
Tactic: have := Fact.mk (Ne.isUnit h3)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : j = 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
this : Fact (IsUnit.{u_2} (M := F) 3)
⊢ (ofJ j).IsElliptic
have neg : (ofJ0 F).IsElliptic
Tactic: rw [h0, ofJ_0_of_three_ne_zero h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).IsElliptic
have pos : ∀ (h1728 : j = 1728), (ofJ j).IsElliptic
Tactic: by_cases h1728 : j = 1728
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
pos : ∀ (h1728 : j = 1728), (ofJ j).IsElliptic
⊢ (ofJ j).IsElliptic
have neg : ∀ (h1728 : ¬j = 1728), (ofJ j).IsElliptic
Tactic: by_cases h1728 : j = 1728
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).IsElliptic
have h2 : Ne.{u_2 + 1} (α := F) 2 0
Tactic: have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : Ne.{u_2 + 1} (α := F) 2 0
⊢ (ofJ j).IsElliptic
have this : Fact (IsUnit.{u_2} (M := F) 2)
Tactic: have := Fact.mk h2.isUnit
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : Ne.{u_2 + 1} (α := F) 2 0
this : Fact (IsUnit.{u_2} (M := F) 2)
⊢ (ofJ j).IsElliptic
have pos : (ofJ1728 F).IsElliptic
Tactic: rw [h1728, ofJ_1728_of_two_ne_zero h2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).IsElliptic
have this : Fact (IsUnit j)
Tactic: have := Fact.mk (Ne.isUnit h0)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this : Fact (IsUnit j)
⊢ (ofJ j).IsElliptic
have this₁ : Fact (IsUnit (j - 1728))
Tactic: have := Fact.mk (sub_ne_zero.2 h1728).isUnit
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
F : Type u_2
inst_2 : Field F
j : F
inst_3 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this_1 : Fact (IsUnit j)
this : Fact (IsUnit (j - 1728))
⊢ (ofJ j).IsElliptic
have neg : (ofJNe0Or1728 j).IsElliptic
Tactic: rw [ofJ_ne_0_ne_1728 j h0 h1728]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
⊢ (ofJ j).j = j
have pos : ∀ (h0 : j = 0), (ofJ j).j = j
Tactic: by_cases h0 : j = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
pos : ∀ (h0 : j = 0), (ofJ j).j = j
⊢ (ofJ j).j = j
have neg : ∀ (h0 : ¬j = 0), (ofJ j).j = j
Tactic: by_cases h0 : j = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j = 0
⊢ (ofJ j).j = j
have pos : ∀ (h3 : Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).j = j
Tactic: by_cases h3 : (3 : F) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j = 0
pos : ∀ (h3 : Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).j = j
⊢ (ofJ j).j = j
have neg : ∀ (h3 : ¬Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).j = j
Tactic: by_cases h3 : (3 : F) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j = 0
h3 : Eq.{u_2 + 1} (α := F) 3 0
⊢ (ofJ j).j = j
have this : Fact (IsUnit.{u_2} (M := F) 2)
Tactic: have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j = 0
h3 : Eq.{u_2 + 1} (α := F) 3 0
this : Fact (IsUnit.{u_2} (M := F) 2)
⊢ (ofJ j).j = j
have pos : Eq.{u_2 + 1} (α := F) 1728 0
Tactic: simp_rw [h0, ofJ_0_of_three_eq_zero h3, ofJ1728_j]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j = 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
⊢ (ofJ j).j = j
have this : Fact (IsUnit.{u_2} (M := F) 3)
Tactic: have := Fact.mk (Ne.isUnit h3)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j = 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
this : Fact (IsUnit.{u_2} (M := F) 3)
⊢ (ofJ j).j = j
have neg : Eq.{u_2 + 1} (α := F) (WeierstrassCurve.j (ofJ 0)) 0
Tactic: simp_rw [h0, ofJ_0_of_three_ne_zero h3, ofJ0_j]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : j = 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
this : Fact (IsUnit.{u_2} (M := F) 3)
neg : Eq.{u_2 + 1} (α := F) (WeierstrassCurve.j (ofJ 0)) 0
⊢ (ofJ j).j = j
have neg₁ : (ofJ0 F).j = 0
Tactic: simp_rw [h0, ofJ_0_of_three_ne_zero h3, ofJ0_j]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).j = j
have pos : ∀ (h1728 : j = 1728), (ofJ j).j = j
Tactic: by_cases h1728 : j = 1728
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
pos : ∀ (h1728 : j = 1728), (ofJ j).j = j
⊢ (ofJ j).j = j
have neg : ∀ (h1728 : ¬j = 1728), (ofJ j).j = j
Tactic: by_cases h1728 : j = 1728
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).j = j
have h2 : Ne.{u_2 + 1} (α := F) 2 0
Tactic: have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : Ne.{u_2 + 1} (α := F) 2 0
⊢ (ofJ j).j = j
have this : Fact (IsUnit.{u_2} (M := F) 2)
Tactic: have := Fact.mk h2.isUnit
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : Ne.{u_2 + 1} (α := F) 2 0
this : Fact (IsUnit.{u_2} (M := F) 2)
⊢ (ofJ j).j = j
have pos : Eq.{u_2 + 1} (α := F) (WeierstrassCurve.j (ofJ 1728)) 1728
Tactic: simp_rw [h1728, ofJ_1728_of_two_ne_zero h2, ofJ1728_j]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : Ne.{u_2 + 1} (α := F) 2 0
this : Fact (IsUnit.{u_2} (M := F) 2)
pos : Eq.{u_2 + 1} (α := F) (WeierstrassCurve.j (ofJ 1728)) 1728
⊢ (ofJ j).j = j
have pos₁ : (ofJ1728 F).j = 1728
Tactic: simp_rw [h1728, ofJ_1728_of_two_ne_zero h2, ofJ1728_j]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).j = j
have this : Fact (IsUnit j)
Tactic: have := Fact.mk (Ne.isUnit h0)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (hypothesis)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this : Fact (IsUnit j)
⊢ (ofJ j).j = j
have this₁ : Fact (IsUnit (j - 1728))
Tactic: have := Fact.mk (sub_ne_zero.2 h1728).isUnit
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this_1 : Fact (IsUnit j)
this : Fact (IsUnit (j - 1728))
⊢ (ofJ j).j = j
have neg : (ofJNe0Or1728 j).j = j
Tactic: simp_rw [ofJ_ne_0_ne_1728 j h0 h1728, ofJNe0Or1728_j]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.b₂ = 4 * W.a₂
have rw : HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₂ = 4 * W.a₂
Tactic: rw [b₂, a₁_of_isCharNeTwoNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.b₄ = 2 * W.a₄
have rw : 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄
Tactic: rw [b₄, a₃_of_isCharNeTwoNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.b₆ = 4 * W.a₆
have rw : HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₆ = 4 * W.a₆
Tactic: rw [b₆, a₃_of_isCharNeTwoNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.b₈ = 4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2
have rw : HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₆ + 4 * W.a₂ * W.a₆ - HMul.hMul (α := R) 0 0 * W.a₄ +
      W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
    HPow.hPow (β := ℕ) W.a₄ 2 =
  4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2
Tactic: rw [b₈, a₁_of_isCharNeTwoNF, a₃_of_isCharNeTwoNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.c₄ = 16 * HPow.hPow (β := ℕ) W.a₂ 2 - 48 * W.a₄
have rw : HPow.hPow (β := ℕ) (4 * W.a₂) 2 - 24 * (2 * W.a₄) = 16 * HPow.hPow (β := ℕ) W.a₂ 2 - 48 * W.a₄
Tactic: rw [c₄, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.c₆ = -64 * HPow.hPow (β := ℕ) W.a₂ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆
have rw : -HPow.hPow (β := ℕ) (4 * W.a₂) 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) =
  -64 * HPow.hPow (β := ℕ) W.a₂ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆
Tactic: rw [c₆, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.Δ =
    -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ + 16 * HPow.hPow (β := ℕ) W.a₂ 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
          64 * HPow.hPow (β := ℕ) W.a₄ 3 -
        432 * HPow.hPow (β := ℕ) W.a₆ 2 +
      288 * W.a₂ * W.a₄ * W.a₆
have rw : -HPow.hPow (β := ℕ) (4 * W.a₂) 2 * (4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2) - 8 * HPow.hPow (β := ℕ) (2 * W.a₄) 3 -
      27 * HPow.hPow (β := ℕ) (4 * W.a₆) 2 +
    9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
  -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ + 16 * HPow.hPow (β := ℕ) W.a₂ 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
        64 * HPow.hPow (β := ℕ) W.a₄ 3 -
      432 * HPow.hPow (β := ℕ) W.a₆ 2 +
    288 * W.a₂ * W.a₄ * W.a₆
Tactic: rw [Δ, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF, b₈_of_isCharNeTwoNF]
-- 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
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).IsCharNeTwoNF
have a₁ : (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
a₁ : (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).IsCharNeTwoNF
have a₃ : (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.IsShortNF
⊢ W.Δ = -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)
have rw : -64 * HPow.hPow (α := R) (β := ℕ) 0 3 * W.a₆ + 16 * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
        64 * HPow.hPow (β := ℕ) W.a₄ 3 -
      432 * HPow.hPow (β := ℕ) W.a₆ 2 +
    HMul.hMul (α := R) 288 0 * W.a₄ * W.a₆ =
  -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)
Tactic: rw [Δ_of_isCharNeTwoNF, a₂_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.b₄ = -W.a₄
have rw : 2 * W.a₄ = -W.a₄
Tactic: rw [b₄_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.b₆ = W.a₆
have rw : 4 * W.a₆ = W.a₆
Tactic: rw [b₆_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.c₄ = 0
have rw : -48 * W.a₄ = 0
Tactic: rw [c₄_of_isShortNF]