awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).neg P
⊢ (W'⁄B).neg ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).neg P
have rw₁ : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((W'⁄A).map (↑f : A →+* B)).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_neg, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).neg P
rw₁ :
  (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).neg ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).neg P
have rw₂ : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_neg, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R F
inst_6 : Algebra S F
inst_7 : IsScalarTower R S F
inst_8 : Algebra R K
inst_9 : Algebra S K
inst_10 : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q
have rw : (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
  (⇑(↑f : F →+* K) : (a : F) → K) ∘ (W'⁄F).add P Q
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_add _ hP hQ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R F
inst_6 : Algebra S F
inst_7 : IsScalarTower R S F
inst_8 : Algebra R K
inst_9 : Algebra S K
inst_10 : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
rw :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    (⇑(↑f : F →+* K) : (a : F) → K) ∘ (W'⁄F).add P Q
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q
have rw₁ : (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
  ((W'⁄F).map (↑f : F →+* K)).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_add _ hP hQ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R F
inst_6 : Algebra S F
inst_7 : IsScalarTower R S F
inst_8 : Algebra R K
inst_9 : Algebra S K
inst_10 : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
rw :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    (⇑(↑f : F →+* K) : (a : F) → K) ∘ (W'⁄F).add P Q
rw₁ :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    ((W'⁄F).map (↑f : F →+* K)).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q
have rw₂ : (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_add _ hP hQ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ (ofJ0 R).c₄ = 0
have rw : HPow.hPow (β := ℕ)
      (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
        HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
      2 -
    24 *
      (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
        HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
          (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) =
  0
Tactic: rw [ofJ0, c₄, b₂, b₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ (ofJ0 R).Δ = -27
have rw : -HPow.hPow (β := ℕ)
              (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
                HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
              2 *
          (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 *
                    a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } +
                  HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) *
                    a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } -
                HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                    (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) *
                  a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } +
              a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } *
                HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                  2 -
            HPow.hPow (α := R) (β := ℕ) (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2) -
        8 *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
              HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
            3 -
      27 *
        HPow.hPow (β := ℕ)
          (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
            HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
          2 +
    9 *
          (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
            HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) *
        (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
          HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
            (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) *
      (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
        HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) =
  -27
Tactic: rw [ofJ0, Δ, b₂, b₄, b₆, b₈]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ (ofJ1728 R).c₄ = -48
have rw : HPow.hPow (β := ℕ)
      (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
        HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
      2 -
    24 *
      (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
        HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
          (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) =
  -48
Tactic: rw [ofJ1728, c₄, b₂, b₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ (ofJ1728 R).Δ = -64
have rw : -HPow.hPow (β := ℕ)
              (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
                HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
              2 *
          (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 *
                    a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } +
                  HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) *
                    a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } -
                HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                    (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) *
                  a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } +
              a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } *
                HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                  2 -
            HPow.hPow (α := R) (β := ℕ) (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2) -
        8 *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
              HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
            3 -
      27 *
        HPow.hPow (β := ℕ)
          (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
            HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
          2 +
    9 *
          (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
            HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) *
        (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
          HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
            (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) *
      (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
        HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) =
  -64
Tactic: rw [ofJ1728, Δ, b₂, b₄, b₆, b₈]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
j : R
⊢ (ofJNe0Or1728 j).c₄ = j * HPow.hPow (β := ℕ) (j - 1728) 3
have simp : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) 2 -
    24 * (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) =
  j * HPow.hPow (β := ℕ) (j - 1728) 3
Tactic: simp only [ofJNe0Or1728, c₄, b₂, b₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
j : R
⊢ (ofJNe0Or1728 j).Δ = HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9
have simp : -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) 2 *
          (HPow.hPow (β := ℕ) (j - 1728) 2 * -HPow.hPow (β := ℕ) (j - 1728) 5 +
                  HMul.hMul (α := R) 4 0 * -HPow.hPow (β := ℕ) (j - 1728) 5 -
                (j - 1728) * 0 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) +
              0 * HPow.hPow (α := R) (β := ℕ) 0 2 -
            HPow.hPow (β := ℕ) (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) 2) -
        8 * HPow.hPow (β := ℕ) (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) 3 -
      27 * HPow.hPow (β := ℕ) (HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * -HPow.hPow (β := ℕ) (j - 1728) 5) 2 +
    9 * (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) *
        (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) *
      (HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * -HPow.hPow (β := ℕ) (j - 1728) 5) =
  HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9
Tactic: simp only [ofJNe0Or1728, Δ, b₂, b₄, b₆, b₈]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 3)
⊢ (ofJ0 R).IsElliptic
have rw : IsUnit.{u_1} (M := R) (-27)
Tactic: rw [isElliptic_iff, ofJ0_Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 3)
⊢ IsUnit.{u_1} (M := R) (-27)
have h : 27 = HPow.hPow (α := R) (β := ℕ) 3 3
Tactic: convert! (hu.out.pow 3).neg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (IsUnit.{u_1} (M := R) 3)
⊢ (ofJ0 R).j = 0
have rw : (↑(ofJ0 R).Δ'⁻¹ : R) * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
Tactic: rw [j, ofJ0_c₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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)
⊢ (ofJ1728 R).IsElliptic
have rw : IsUnit.{u_1} (M := R) (-64)
Tactic: rw [isElliptic_iff, ofJ1728_Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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)
⊢ IsUnit.{u_1} (M := R) (-64)
have h : 64 = HPow.hPow (α := R) (β := ℕ) 2 6
Tactic: convert! (hu.out.pow 6).neg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (IsUnit.{u_1} (M := R) 2)
⊢ (ofJ1728 R).j = 1728
have rw : HPow.hPow (α := R) (β := ℕ) (-48) 3 = HMul.hMul (α := R) (-64) 1728
Tactic: rw [j, Units.inv_mul_eq_iff_eq_mul, ofJ1728_c₄, coe_Δ', ofJ1728_Δ]
-- 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
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).IsElliptic
have rw : IsUnit (HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9)
Tactic: rw [isElliptic_iff, ofJNe0Or1728_Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
R : Type u_1
inst : CommRing R
j : R
inst_1 : Fact (IsUnit j)
inst_2 : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).j = j
have rw : HPow.hPow (β := ℕ) (j * HPow.hPow (β := ℕ) (j - 1728) 3) 3 =
  HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9 * j
Tactic: rw [WeierstrassCurve.j, Units.inv_mul_eq_iff_eq_mul, ofJNe0Or1728_c₄, coe_Δ', ofJNe0Or1728_Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h3 : Ne.{u_2 + 1} (α := F) 3 0
⊢ ofJ 0 = ofJ0 F
have 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
Tactic: rw [ofJ, if_pos rfl, if_neg h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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
⊢ ofJ 0 = 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 rfl, if_neg h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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
⊢ ofJ 0 = ofJ0 F
have rw₂ : ofJ0 F = ofJ0 F
Tactic: rw [ofJ, if_pos rfl, if_neg h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
Goal:
F : Type u_2
inst : Field F
inst_1 : DecidableEq F
h3 : Eq.{u_2 + 1} (α := F) 3 0
⊢ ofJ 0 = ofJ1728 F
have 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
Tactic: rw [ofJ, if_pos rfl, if_pos h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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
⊢ ofJ 0 = ofJ1728 F
have rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ1728 F
Tactic: rw [ofJ, if_pos rfl, if_pos h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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
⊢ ofJ 0 = ofJ1728 F
have rw₂ : ofJ1728 F = ofJ1728 F
Tactic: rw [ofJ, if_pos rfl, if_pos h3]
-- 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 0 = ofJ0 F
have 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
Tactic: rw [ofJ, if_pos rfl, 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) 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
⊢ ofJ 0 = 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 rfl, 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) 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
⊢ ofJ 0 = ofJ0 F
have rw₂ : ofJ0 F = ofJ0 F
Tactic: rw [ofJ, if_pos rfl, 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
h3 : Eq.{u_2 + 1} (α := F) 3 0
⊢ ofJ 1728 = ofJ1728 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) =
  ofJ1728 F
Tactic: rw [ofJ, if_pos (by linear_combination 576 * h3), if_pos h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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
⊢ ofJ 1728 = ofJ1728 F
have rw₁ : (if Eq.{u_2 + 1} (α := F) 3 0 then ofJ1728 F else ofJ0 F) = ofJ1728 F
Tactic: rw [ofJ, if_pos (by linear_combination 576 * h3), if_pos h3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ (goal)
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
⊢ ofJ 1728 = ofJ1728 F
have rw₂ : ofJ1728 F = ofJ1728 F
Tactic: rw [ofJ, if_pos (by linear_combination 576 * h3), if_pos h3]
-- 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
⊢ ofJ 1728 = ofJ1728 F
have pos : ∀ (h3 : Eq.{u_2 + 1} (α := F) 3 0), ofJ 1728 = ofJ1728 F
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
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
⊢ ofJ 1728 = ofJ1728 F
have neg : ∀ (h3 : ¬Eq.{u_2 + 1} (α := F) 3 0), ofJ 1728 = ofJ1728 F
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
inst_1 : DecidableEq F
h2 : Ne.{u_2 + 1} (α := F) 2 0
h3 : ¬Eq.{u_2 + 1} (α := F) 3 0
⊢ ofJ 1728 = ofJ1728 F
have 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
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]