awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 2)
h : 64 = HPow.hPow (α := R) (β := ℕ) 2 6
⊢ IsUnit.{u_1} (M := R) (-64)

Tactic:
convert! (hu.out.pow 6).neg

Premises used: IsUnit.pow, IsUnit.neg, OfNat.ofNat, Fact.out
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 2)
⊢ 64 = HPow.hPow (α := R) (β := ℕ) 2 6

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (IsUnit.{u_1} (M := R) 2)
rw : HPow.hPow (α := R) (β := ℕ) (-48) 3 = HMul.hMul (α := R) (-64) 1728
⊢ (ofJ1728 R).j = 1728

Tactic:
rw [j, Units.inv_mul_eq_iff_eq_mul, ofJ1728_c₄, coe_Δ', ofJ1728_Δ]

Premises used: WeierstrassCurve.j, WeierstrassCurve.coe_Δ', Units.inv_mul_eq_iff_eq_mul, WeierstrassCurve.ofJ1728_Δ, WeierstrassCurve.ofJ1728_c₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (IsUnit.{u_1} (M := R) 2)
⊢ HPow.hPow (α := R) (β := ℕ) (-48) 3 = HMul.hMul (α := R) (-64) 1728

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
rw : IsUnit (HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9)
⊢ (ofJNe0Or1728 j).IsElliptic

Tactic:
rw [isElliptic_iff, ofJNe0Or1728_Δ]

Premises used: WeierstrassCurve.ofJNe0Or1728_Δ, WeierstrassCurve.isElliptic_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9)

Tactic:
(h1.out.pow 2).mul (h2.out.pow 9)

Premises used: IsUnit.mul, IsUnit.pow, OfNat.ofNat, Fact.out
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j_1 : R
inst_1 : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9)

Tactic:
exact (h1.out.pow 2).mul (h2.out.pow 9)

Premises used: IsUnit.mul, IsUnit.pow, OfNat.ofNat, Fact.out
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
j : R
inst_1 : Fact (IsUnit j)
inst_2 : Fact (IsUnit (j - 1728))
rw :
  HPow.hPow (β := ℕ) (j * HPow.hPow (β := ℕ) (j - 1728) 3) 3 =
    HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9 * j
⊢ (ofJNe0Or1728 j).j = j

Tactic:
rw [WeierstrassCurve.j, Units.inv_mul_eq_iff_eq_mul, ofJNe0Or1728_c₄, coe_Δ', ofJNe0Or1728_Δ]

Premises used: WeierstrassCurve.ofJNe0Or1728_Δ, WeierstrassCurve.ofJNe0Or1728_c₄, WeierstrassCurve.j, WeierstrassCurve.coe_Δ', Units.inv_mul_eq_iff_eq_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
j : R
inst_1 : Fact (IsUnit j)
inst_2 : Fact (IsUnit (j - 1728))
⊢ HPow.hPow (β := ℕ) (j * HPow.hPow (β := ℕ) (j - 1728) 3) 3 =
    HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9 * j

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h3 : Ne.{u_2 + 1} (α := F) 3 0
rw :
  (if Eq.{u_2 + 1} (α := F) 0 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 0 1728 then ofJ1728 F else ofJNe0Or1728 0) =
    ofJ0 F
rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ0 F
rw₂ rw₃ : ofJ0 F = ofJ0 F
⊢ ofJ 0 = ofJ0 F

Tactic:
rw [ofJ, if_pos rfl, if_neg h3]

Premises used: WeierstrassCurve.ofJ, if_pos, if_neg, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h3 : Eq.{u_2 + 1} (α := F) 3 0
rw :
  (if Eq.{u_2 + 1} (α := F) 0 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 0 1728 then ofJ1728 F else ofJNe0Or1728 0) =
    ofJ1728 F
rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ1728 F
rw₂ rw₃ : ofJ1728 F = ofJ1728 F
⊢ ofJ 0 = ofJ1728 F

Tactic:
rw [ofJ, if_pos rfl, if_pos h3]

Premises used: WeierstrassCurve.ofJ, if_pos, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Eq.{u_2 + 1} (α := F) 2 0
⊢ Eq.{u_2 + 1} (α := F) 3 1

Tactic:
linear_combination h2
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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) 0 0 then if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F
    else if Eq.{u_2 + 1} (α := F) 0 1728 then ofJ1728 F else ofJNe0Or1728 0) =
    ofJ0 F
rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ0 F
rw₂ rw₃ : ofJ0 F = ofJ0 F
⊢ ofJ 0 = ofJ0 F

Tactic:
rw [ofJ, if_pos rfl, if_neg ((show (3 : F) = 1 by linear_combination h2) ▸ one_ne_zero)]

Premises used: WeierstrassCurve.ofJ, if_pos, if_neg, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h3 : Eq.{u_2 + 1} (α := F) 3 0
⊢ Eq.{u_2 + 1} (α := F) 1728 0

Tactic:
linear_combination 576 * h3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h3 : Eq.{u_2 + 1} (α := F) 3 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) =
    ofJ1728 F
rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ1728 F
rw₂ rw₃ : ofJ1728 F = ofJ1728 F
⊢ ofJ 1728 = ofJ1728 F

Tactic:
rw [ofJ, if_pos (by linear_combination 576 * h3), if_pos h3]

Premises used: WeierstrassCurve.ofJ, if_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Ne.{u_2 + 1} (α := F) 2 0
pos : ∀ (h3 : Eq.{u_2 + 1} (α := F) 3 0), ofJ 1728 = ofJ1728 F
neg : ∀ (h3 : ¬Eq.{u_2 + 1} (α := F) 3 0), ofJ 1728 = ofJ1728 F
⊢ ofJ 1728 = ofJ1728 F

Tactic:
by_cases h3 : (3 : F) = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ ofJ 1728 = ofJ1728 F

Tactic:
ofJ_1728_of_three_eq_zero h3

Premises used: WeierstrassCurve.ofJ_1728_of_three_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ ofJ 1728 = ofJ1728 F

Tactic:
exact ofJ_1728_of_three_eq_zero h3

Premises used: WeierstrassCurve.ofJ_1728_of_three_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ 1728 = HPow.hPow (α := F) (β := ℕ) 2 6 * HPow.hPow (α := F) (β := ℕ) 3 3

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
neg₃ neg₄ : ofJ1728 F = ofJ1728 F
⊢ ofJ 1728 = 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]

Premises used: WeierstrassCurve.ofJ, pow_ne_zero, if_pos, mul_ne_zero, OfNat.ofNat, if_neg, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h2 : Eq.{u_2 + 1} (α := F) 2 0
⊢ Eq.{u_2 + 1} (α := F) 1728 0

Tactic:
linear_combination 864 * h2
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
rw₂ rw₃ : ofJ0 F = ofJ0 F
⊢ ofJ 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)]

Premises used: WeierstrassCurve.ofJ, if_pos, if_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
rw₂ rw₃ : ofJNe0Or1728 j = ofJNe0Or1728 j
⊢ ofJ j = ofJNe0Or1728 j

Tactic:
rw [ofJ, if_neg h0, if_neg h1728]

Premises used: WeierstrassCurve.ofJ, if_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
neg : ∀ (h0 : ¬j = 0), (ofJ j).IsElliptic
⊢ (ofJ j).IsElliptic

Tactic:
by_cases h0 : j = 0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
neg : ∀ (h3 : ¬Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).IsElliptic
⊢ (ofJ j).IsElliptic

Tactic:
by_cases h3 : (3 : F) = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ HMul.hMul (α := F) 2 2 = 1

Tactic:
linear_combination h3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Fact (IsUnit.{u_2} (M := F) 2)

Tactic:
have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
pos : (ofJ1728 F).IsElliptic
⊢ (ofJ j).IsElliptic

Tactic:
rw [h0, ofJ_0_of_three_eq_zero h3]

Premises used: WeierstrassCurve.ofJ_0_of_three_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
⊢ (ofJ1728 F).IsElliptic

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Fact (IsUnit.{u_2} (M := F) 3)

Tactic:
have := Fact.mk (Ne.isUnit h3)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
neg : (ofJ0 F).IsElliptic
⊢ (ofJ j).IsElliptic

Tactic:
rw [h0, ofJ_0_of_three_ne_zero h3]

Premises used: WeierstrassCurve.ofJ_0_of_three_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
⊢ (ofJ0 F).IsElliptic

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
neg : ∀ (h1728 : ¬j = 1728), (ofJ j).IsElliptic
⊢ (ofJ j).IsElliptic

Tactic:
by_cases h1728 : j = 1728
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
h : Eq.{u_2 + 1} (α := F) 2 0
⊢ j = 0

Tactic:
linear_combination h1728 + 864 * h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Ne.{u_2 + 1} (α := F) 2 0

Tactic:
have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Fact (IsUnit.{u_2} (M := F) 2)

Tactic:
have := Fact.mk h2.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
pos : (ofJ1728 F).IsElliptic
⊢ (ofJ j).IsElliptic

Tactic:
rw [h1728, ofJ_1728_of_two_ne_zero h2]

Premises used: WeierstrassCurve.ofJ_1728_of_two_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
⊢ (ofJ1728 F).IsElliptic

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Fact (IsUnit j)

Tactic:
have := Fact.mk (Ne.isUnit h0)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
⊢ Fact (IsUnit (j - 1728))

Tactic:
have := Fact.mk (sub_ne_zero.2 h1728).isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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))
neg : (ofJNe0Or1728 j).IsElliptic
⊢ (ofJ j).IsElliptic

Tactic:
rw [ofJ_ne_0_ne_1728 j h0 h1728]

Premises used: WeierstrassCurve.ofJ_ne_0_ne_1728
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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))
⊢ (ofJNe0Or1728 j).IsElliptic

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
pos : ∀ (h0 : j = 0), (ofJ j).j = j
neg : ∀ (h0 : ¬j = 0), (ofJ j).j = j
⊢ (ofJ j).j = j

Tactic:
by_cases h0 : j = 0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
neg : ∀ (h3 : ¬Eq.{u_2 + 1} (α := F) 3 0), (ofJ j).j = j
⊢ (ofJ j).j = j

Tactic:
by_cases h3 : (3 : F) = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ HMul.hMul (α := F) 2 2 = 1

Tactic:
linear_combination h3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Fact (IsUnit.{u_2} (M := F) 2)

Tactic:
have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
pos : Eq.{u_2 + 1} (α := F) 1728 0
⊢ (ofJ j).j = j

Tactic:
simp_rw [h0, ofJ_0_of_three_eq_zero h3, ofJ1728_j]

Premises used: WeierstrassCurve.ofJ1728_j, WeierstrassCurve.ofJ_0_of_three_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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)
⊢ Eq.{u_2 + 1} (α := F) 1728 0

Tactic:
linear_combination 576 * h3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Fact (IsUnit.{u_2} (M := F) 3)

Tactic:
have := Fact.mk (Ne.isUnit h3)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
neg₁ : (ofJ0 F).j = 0
⊢ (ofJ j).j = j

Tactic:
simp_rw [h0, ofJ_0_of_three_ne_zero h3, ofJ0_j]

Premises used: WeierstrassCurve.ofJ0_j, WeierstrassCurve.ofJ_0_of_three_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
neg : ∀ (h1728 : ¬j = 1728), (ofJ j).j = j
⊢ (ofJ j).j = j

Tactic:
by_cases h1728 : j = 1728
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h : Eq.{u_2 + 1} (α := F) 2 0
⊢ j = 0

Tactic:
linear_combination h1728 + 864 * h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ Ne.{u_2 + 1} (α := F) 2 0

Tactic:
have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
⊢ Fact (IsUnit.{u_2} (M := F) 2)

Tactic:
have := Fact.mk h2.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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
pos₁ : (ofJ1728 F).j = 1728
⊢ (ofJ j).j = j

Tactic:
simp_rw [h1728, ofJ_1728_of_two_ne_zero h2, ofJ1728_j]

Premises used: WeierstrassCurve.ofJ_1728_of_two_ne_zero, WeierstrassCurve.ofJ1728_j
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ Fact (IsUnit j)

Tactic:
have := Fact.mk (Ne.isUnit h0)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
F : Type u_2
inst : Field F
j : F
inst_1 : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this : Fact (IsUnit j)
⊢ Fact (IsUnit (j - 1728))

Tactic:
have := Fact.mk (sub_ne_zero.2 h1728).isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
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))
neg : (ofJNe0Or1728 j).j = j
⊢ (ofJ j).j = j

Tactic:
simp_rw [ofJ_ne_0_ne_1728 j h0 h1728, ofJNe0Or1728_j]

Premises used: WeierstrassCurve.ofJ_ne_0_ne_1728, WeierstrassCurve.ofJNe0Or1728_j
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.a₁ = 0

Tactic:
IsCharNeTwoNF.a₁

Premises used: WeierstrassCurve.IsCharNeTwoNF.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ W.a₃ = 0

Tactic:
IsCharNeTwoNF.a₃

Premises used: WeierstrassCurve.IsCharNeTwoNF.a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
rw : HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₂ = 4 * W.a₂
⊢ W.b₂ = 4 * W.a₂

Tactic:
rw [b₂, a₁_of_isCharNeTwoNF]

Premises used: WeierstrassCurve.a₁_of_isCharNeTwoNF, WeierstrassCurve.b₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₂ = 4 * W.a₂

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
rw : 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄
⊢ W.b₄ = 2 * W.a₄

Tactic:
rw [b₄, a₃_of_isCharNeTwoNF]

Premises used: WeierstrassCurve.b₄, WeierstrassCurve.a₃_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
rw : HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₆ = 4 * W.a₆
⊢ W.b₆ = 4 * W.a₆

Tactic:
rw [b₆, a₃_of_isCharNeTwoNF]

Premises used: WeierstrassCurve.a₃_of_isCharNeTwoNF, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₆ = 4 * W.a₆

Tactic:
ring1