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
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) n =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) n
have h : ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) =
  HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
    ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
h :
  ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) n =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) n
have h₁ : ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) =
  HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
    ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
h :
  ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))
h₁ :
  ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) n =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) n
have h₂ : ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) =
  HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
    ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))
have h : Matrix.vecCons (n := (Nat.succ 0).succ) ((f : (a : R) → S) (HPow.hPow (β := ℕ) u 2 * P x))
    ![(f : (a : R) → S) (HPow.hPow (β := ℕ) u 3 * P y), (f : (a : R) → S) (u * P z)] ⟨0, sorry⟩ =
  ![HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) u : S) 2 * ((⇑f : (a : R) → S) ∘ P) x,
      HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) u : S) 3 * ((⇑f : (a : R) → S) ∘ P) y,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) u : S) (((⇑f : (a : R) → S) ∘ P) z : S)]
    (⟨0, sorry⟩ : Fin 3)
Tactic: simp only [smul_fin3, comp_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))
have h : Matrix.vecCons (n := (Nat.succ 0).succ) ((f : (a : R) → S) (HPow.hPow (β := ℕ) u 2 * P x))
    ![(f : (a : R) → S) (HPow.hPow (β := ℕ) u 3 * P y), (f : (a : R) → S) (u * P z)] ⟨1, sorry⟩ =
  ![HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) u : S) 2 * ((⇑f : (a : R) → S) ∘ P) x,
      HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) u : S) 3 * ((⇑f : (a : R) → S) ∘ P) y,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) u : S) (((⇑f : (a : R) → S) ∘ P) z : S)]
    (⟨1, sorry⟩ : Fin 3)
Tactic: simp only [smul_fin3, comp_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))
have h : Matrix.vecCons (n := (Nat.succ 0).succ) ((f : (a : R) → S) (HPow.hPow (β := ℕ) u 2 * P x))
    ![(f : (a : R) → S) (HPow.hPow (β := ℕ) u 3 * P y), (f : (a : R) → S) (u * P z)] ⟨2, sorry⟩ =
  ![HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) u : S) 2 * ((⇑f : (a : R) → S) ∘ P) x,
      HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) u : S) 3 * ((⇑f : (a : R) → S) ∘ P) y,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) u : S) (((⇑f : (a : R) → S) ∘ P) z : S)]
    (⟨2, sorry⟩ : Fin 3)
Tactic: simp only [smul_fin3, comp_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u • P ≈ v • Q ↔ P ≈ Q
have rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
Tactic: rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
⊢ u • P ≈ v • Q ↔ P ≈ Q
have rw₁ : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
Tactic: rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
rw₁ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
⊢ u • P ≈ v • Q ↔ P ≈ Q
have rw₂ : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦v • Q⟧ ↔
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
Tactic: rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
rw₁ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
rw₂ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦v • Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
⊢ u • P ≈ v • Q ↔ P ≈ Q
have rw₃ : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧ ↔
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
Tactic: rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (Q z)
⊢ P ≈ Q ↔ P = Q
have refine : P ≈ Q → P = Q
Tactic: refine ⟨?_, Quotient.exact.comp <| congrArg _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
hQz : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (Q z)
u : Rˣ
hz : (fun (m : Rˣ) ↦ m • Q) u z = Q z
⊢ (fun (m : Rˣ) ↦ m • Q) u = Q
have simp : HSMul.hSMul (α := R) 1 Q = Q
Tactic: simp only [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors hQz).mp <| one_mul (Q z) ▸ hz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
hQz : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (Q z)
u : Rˣ
hz : (fun (m : Rˣ) ↦ m • Q) u z = Q z
⊢ HSMul.hSMul (α := R) 1 Q = Q
have rw : Q = Q
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P z = 0 ↔ Q z = 0
have rcases : ∀ (w : Rˣ), Eq.{r + 1} (α := R) ((fun (m : Rˣ) ↦ m • Q) w z) 0 ↔ Q z = 0
Tactic: rcases h with ⟨_, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
have rcases : ∀ (u : Rˣ),
  (fun (m : Rˣ) ↦ m • Q) u x * HPow.hPow (β := ℕ) (Q z) 2 =
    Q x * HPow.hPow (α := R) (β := ℕ) ((fun (m : Rˣ) ↦ m • Q) u z) 2
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun (m : Rˣ) ↦ m • Q) u x * HPow.hPow (β := ℕ) (Q z) 2 =
    Q x * HPow.hPow (α := R) (β := ℕ) ((fun (m : Rˣ) ↦ m • Q) u z) 2
have simp : HPow.hPow (β := ℕ) (↑u : R) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) ((↑u : R) * Q z) 2
Tactic: simp only [Units.smul_def, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
have rcases : ∀ (u : Rˣ),
  (fun (m : Rˣ) ↦ m • Q) u y * HPow.hPow (β := ℕ) (Q z) 3 =
    Q y * HPow.hPow (α := R) (β := ℕ) ((fun (m : Rˣ) ↦ m • Q) u z) 3
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun (m : Rˣ) ↦ m • Q) u y * HPow.hPow (β := ℕ) (Q z) 3 =
    Q y * HPow.hPow (α := R) (β := ℕ) ((fun (m : Rˣ) ↦ m • Q) u z) 3
have simp : HPow.hPow (β := ℕ) (↑u : R) 3 * Q y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) ((↑u : R) * Q z) 3
Tactic: simp only [Units.smul_def, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
⊢ P ≈ Q
have h : (fun (m : Fˣ) ↦ m • Q) (HDiv.hDiv (α := Fˣ) (Units.mk0 (P z) hPz) (Units.mk0 (Q z) hQz)) = P
Tactic: use Units.mk0 _ hPz / Units.mk0 _ hQz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * HPow.hPow (β := ℕ) (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] z) 2 + -P x * 1 -
      (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] x * HPow.hPow (β := ℕ) (P z) 2 +
        -P x * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) =
    0
have a : P x * HPow.hPow (α := F) (β := ℕ) 1 2 + -P x * 1 -
    (P x / HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P z) 2 +
      -P x * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) =
  0
Tactic: matrix_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * HPow.hPow (β := ℕ) (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] z) 2 =
    ![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] x * HPow.hPow (β := ℕ) (P z) 2
have a : P x * HPow.hPow (β := ℕ) (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] z) 2 + -P x * 1 -
    (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] x * HPow.hPow (β := ℕ) (P z) 2 +
      -P x * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) =
  0
Tactic: linear_combination (norm := (matrix_simp; ring1)) -P x * div_self (pow_ne_zero 2 hPz)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * HPow.hPow (β := ℕ) (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] z) 3 + -P y * 1 -
      (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] y * HPow.hPow (β := ℕ) (P z) 3 +
        -P y * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) =
    0
have a : P y * HPow.hPow (α := F) (β := ℕ) 1 3 + -P y * 1 -
    (P y / HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (P z) 3 +
      -P y * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) =
  0
Tactic: matrix_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * HPow.hPow (β := ℕ) (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] z) 3 =
    ![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] y * HPow.hPow (β := ℕ) (P z) 3
have a : P y * HPow.hPow (β := ℕ) (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] z) 3 + -P y * 1 -
    (![P x / HPow.hPow (β := ℕ) (P z) 2, P y / HPow.hPow (β := ℕ) (P z) 3, 1] y * HPow.hPow (β := ℕ) (P z) 3 +
      -P y * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) =
  0
Tactic: linear_combination (norm := (matrix_simp; ring1)) -P y * div_self (pow_ne_zero 3 hPz)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial =
    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)
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
              Y *
            Z +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) Y *
          HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3 -
      (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 3 +
            HMul.hMul (α := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₂ : MvPolynomial (Fin 3) R)
                (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) *
              HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R) X *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 4 +
        HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₆ : MvPolynomial (Fin 3) R)
          (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) 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)
Tactic: rw [polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 6) +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * 1 + W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 *
                (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 6 / HPow.hPow (β := ℕ) (P z) 6)) -
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomial +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * (P z / P z) +
                W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 * 1 +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₆ * 1)) =
    0
have a : (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 +
      (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * 1 + W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 *
              (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4) +
        W.a₆ * (HPow.hPow (β := ℕ) (P z) 6 / HPow.hPow (β := ℕ) (P z) 6)) -
    (HPow.hPow (β := ℕ) (P y / HPow.hPow (β := ℕ) (P z) 3) 2 +
            W.toAffine.a₁ * (P x / HPow.hPow (β := ℕ) (P z) 2) * (P y / HPow.hPow (β := ℕ) (P z) 3) +
          W.toAffine.a₃ * (P y / HPow.hPow (β := ℕ) (P z) 3) -
        (HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 3 +
              W.toAffine.a₂ * HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 2 +
            W.toAffine.a₄ * (P x / HPow.hPow (β := ℕ) (P z) 2) +
          W.toAffine.a₆) +
      (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * (P z / P z) +
              W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3) +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 * 1 +
          W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
        W.a₆ * 1)) =
  0
Tactic: rw [eval_polynomial, Affine.evalEval_polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 6) =
    Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomial
have a : HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 6) +
      (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * 1 + W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 *
              (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4) +
        W.a₆ * (HPow.hPow (β := ℕ) (P z) 6 / HPow.hPow (β := ℕ) (P z) 6)) -
    (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomial +
      (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * (P z / P z) +
              W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3) +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 * 1 +
          W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
        W.a₆ * 1)) =
  0
Tactic: linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
    W.a₁ * P x * P y / P z ^ 5 * div_self hPz + W.a₃ * P y / P z ^ 3 * div_self (pow_ne_zero 3 hPz)
      - W.a₂ * P x ^ 2 / P z ^ 4 * div_self (pow_ne_zero 2 hPz)
      - W.a₄ * P x / P z ^ 2 * div_self (pow_ne_zero 4 hPz) - W.a₆ * div_self (pow_ne_zero 6 hPz)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.Equation P ↔
    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) =
      0
have rw : Eq (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) (0 : R) ↔
  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) =
    0
Tactic: rw [Equation, eval_polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
rw :
  Eq (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) (0 : R) ↔
    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) =
      0
⊢ W'.Equation P ↔
    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) =
      0
have rw₁ : 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) =
    0 ↔
  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) =
    0
Tactic: rw [Equation, eval_polynomial]