awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
h : (W'⁄A).Equation P
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P)
have h₁ : W'⁄B = (W'⁄A).map f.toRingHom
Tactic: convert! Equation.map f.toRingHom h using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
h : (W'⁄A).Equation P
⊢ W'⁄B = (W'⁄A).map f.toRingHom
have h₁ : W'⁄B = (W'⁄A).map (↑f : A →+* B)
Tactic: rw [AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
h : (W'⁄A).Equation P
h₁ : W'⁄B = (W'⁄A).map (↑f : A →+* B)
⊢ W'⁄B = (W'⁄A).map f.toRingHom
have h₂ : W'⁄B = W'⁄B
Tactic: rw [AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw₁ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
rw₁ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw₂ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map (↑f : A →+* B)).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
rw₁ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw₃ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialX)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX ((W'⁄A).map (↑f : A →+* B)).polynomialX
Tactic: rw [← map_polynomialX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX ((W'⁄A).map (↑f : A →+* B)).polynomialX
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialX)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX (W'⁄B).polynomialX
Tactic: rw [← map_polynomialX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialY)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY ((W'⁄A).map (↑f : A →+* B)).polynomialY
Tactic: rw [← map_polynomialY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY ((W'⁄A).map (↑f : A →+* B)).polynomialY
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialY)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY (W'⁄B).polynomialY
Tactic: rw [← map_polynomialY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialZ)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ ((W'⁄A).map (↑f : A →+* B)).polynomialZ
Tactic: rw [← map_polynomialZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ ((W'⁄A).map (↑f : A →+* B)).polynomialZ
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialZ)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ (W'⁄B).polynomialZ
Tactic: rw [← map_polynomialZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw₁ : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
rw₁ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw₂ : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map (↑f : A →+* B)).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
rw₁ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw₃ : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.negY (u • P) = HPow.hPow (β := ℕ) u 3 * W'.negY P
have simp : -(HPow.hPow (β := ℕ) u 3 * P y) - W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) -
    W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 =
  HPow.hPow (β := ℕ) u 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)
Tactic: simp only [negY, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.negY P = -P y
have rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
Tactic: rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
⊢ W'.negY P = -P y
have rw₁ : -P y - W'.a₁ * P x * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
Tactic: rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
rw₁ : -P y - W'.a₁ * P x * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
⊢ W'.negY P = -P y
have rw₂ : -P y - 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
Tactic: rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
rw₁ : -P y - W'.a₁ * P x * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₂ : -P y - 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
⊢ W'.negY P = -P y
have rw₃ : -P y - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
Tactic: rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
rw₁ : -P y - W'.a₁ * P x * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₂ : -P y - 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₃ : -P y - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
⊢ W'.negY P = -P y
have rw₄ : -P y - W'.a₃ * 0 = -P y
Tactic: rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
rw₁ : -P y - W'.a₁ * P x * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₂ : -P y - 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₃ : -P y - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₄ : -P y - W'.a₃ * 0 = -P y
⊢ W'.negY P = -P y
have rw₅ : -P y - 0 = -P y
Tactic: rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
rw₁ : -P y - W'.a₁ * P x * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₂ : -P y - 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₃ : -P y - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₄ : -P y - W'.a₃ * 0 = -P y
rw₅ : -P y - 0 = -P y
⊢ W'.negY P = -P y
have rw₆ : -P y = -P y
Tactic: rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / HPow.hPow (β := ℕ) (P z) 3 +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) + W.a₃ * 1)) =
    0
have a : (-P y - W.a₁ * P x * P z - W.a₃ * HPow.hPow (β := ℕ) (P z) 3) / HPow.hPow (β := ℕ) (P z) 3 +
      (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
        W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
    (-(P y / HPow.hPow (β := ℕ) (P z) 3) - W.toAffine.a₁ * (P x / HPow.hPow (β := ℕ) (P z) 2) - W.toAffine.a₃ +
      (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) + W.a₃ * 1)) =
  0
Tactic: rw [negY, Affine.negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / HPow.hPow (β := ℕ) (P z) 3 =
    W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
have a : W.negY P / HPow.hPow (β := ℕ) (P z) 3 +
      (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
        W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
    (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) +
      (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) + W.a₃ * 1)) =
  0
Tactic: linear_combination (norm := (rw [negY, Affine.negY]; ring1))
    -W.a₁ * P x / P z ^ 2 * div_self hPz - W.a₃ * div_self (pow_ne_zero 3 hPz)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
      (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) =
    0
have a : (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
        (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
      (HPow.hPow (β := ℕ) (Q z) 6 * 0 +
          HPow.hPow (β := ℕ) (P z) 6 *
            (HPow.hPow (β := ℕ) (Q y) 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 3 -
              (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 4 +
                W'.a₆ * HPow.hPow (β := ℕ) (Q z) 6)) +
        (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
                      P x * Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                    HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 4 -
                  W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 4 +
                W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
              W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 2 +
            W'.a₄ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 4) *
          (Q x * HPow.hPow (β := ℕ) (P z) 2)) -
    (0 +
      (HPow.hPow (β := ℕ) (Q z) 6 *
            (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
              (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
                W'.a₆ * HPow.hPow (β := ℕ) (P z) 6)) +
          HPow.hPow (β := ℕ) (P z) 6 * 0 +
        (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
                      P x * Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                    HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 4 -
                  W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 4 +
                W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
              W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 2 +
            W'.a₄ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 4) *
          (P x * HPow.hPow (β := ℕ) (Q z) 2))) =
  0
Tactic: linear_combination (norm := (rw [negY]; ring1)) Q z ^ 6 * (equation_iff P).mp hP
    - P z ^ 6 * (equation_iff Q).mp hQ + (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2
      + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 + W'.a₂ * P x * P z ^ 2 * Q z ^ 4
      + W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 + W'.a₄ * P z ^ 4 * Q z ^ 4) * hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
          (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
        -W'.a₁ * P z * Q z * (Q x * HPow.hPow (β := ℕ) (P z) 2) -
      ((P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3 + -W'.a₁ * P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2)) =
    0
have a : P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
        (P y * HPow.hPow (β := ℕ) (Q z) 3 -
          (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3) * HPow.hPow (β := ℕ) (P z) 3) +
      -W'.a₁ * P z * Q z * (Q x * HPow.hPow (β := ℕ) (P z) 2) -
    ((P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) * HPow.hPow (β := ℕ) (Q z) 3 +
      -W'.a₁ * P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2)) =
  0
Tactic: rw [negY, negY]