awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.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.Projective.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.Projective.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.Projective.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.Projective.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.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P x * Q z = Q x * P z
have rcases : ∀ (u : Rˣ), (fun (m : Rˣ) ↦ m • Q) u x * Q z = Q x * (fun (m : Rˣ) ↦ m • Q) u z
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun (m : Rˣ) ↦ m • Q) u x * Q z = Q x * (fun (m : Rˣ) ↦ m • Q) u z
have simp : (↑u : R) * Q x * Q z = Q x * ((↑u : R) * Q z)
Tactic: simp only [Units.smul_def, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P y * Q z = Q y * P z
have rcases : ∀ (u : Rˣ), (fun (m : Rˣ) ↦ m • Q) u y * Q z = Q y * (fun (m : Rˣ) ↦ m • Q) u z
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun (m : Rˣ) ↦ m • Q) u y * Q z = Q y * (fun (m : Rˣ) ↦ m • Q) u z
have simp : (↑u : R) * Q y * Q z = Q y * ((↑u : R) * Q z)
Tactic: simp only [Units.smul_def, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.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 * Q z = Q x * P z
hy : P y * Q z = Q y * P z
⊢ 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.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z, P y / P z, 1] z + -P x * 1 - (![P x / P z, P y / P z, 1] x * P z + -P x * (P z / P z)) = 0
have a : P x * 1 + -P x * 1 - (P x / P z * P z + -P x * (P z / P z)) = 0
Tactic: matrix_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z, P y / P z, 1] z = ![P x / P z, P y / P z, 1] x * P z
have a : P x * ![P x / P z, P y / P z, 1] z + -P x * 1 - (![P x / P z, P y / P z, 1] x * P z + -P x * (P z / P z)) = 0
Tactic: linear_combination (norm := (matrix_simp; ring1)) -P x * div_self hPz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z, P y / P z, 1] z + -P y * 1 - (![P x / P z, P y / P z, 1] y * P z + -P y * (P z / P z)) = 0
have a : P y * 1 + -P y * 1 - (P y / P z * P z + -P y * (P z / P z)) = 0
Tactic: matrix_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z, P y / P z, 1] z = ![P x / P z, P y / P z, 1] y * P z
have a : P y * ![P x / P z, P y / P z, 1] z + -P y * 1 - (![P x / P z, P y / P z, 1] y * P z + -P y * (P z / P z)) = 0
Tactic: linear_combination (norm := (matrix_simp; ring1)) -P y * div_self hPz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial =
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 * Z +
          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 2 -
      (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) *
              Z +
          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 2 +
        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 3))) =
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
    (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)
Tactic: rw [polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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) 3) +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                W.a₃ * P y / P z * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
            W.a₄ * P x / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                W.a₃ * P y / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0
have a : (HPow.hPow (β := ℕ) (P y) 2 * P z + W.a₁ * P x * P y * P z + W.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (HPow.hPow (β := ℕ) (P x) 3 + W.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
              W.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W.a₆ * HPow.hPow (β := ℕ) (P z) 3)) /
        HPow.hPow (β := ℕ) (P z) 3 +
      (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 + W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * 1 +
              W.a₃ * P y / P z * 1 +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
          W.a₄ * P x / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
        W.a₆ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
    (HPow.hPow (β := ℕ) (P y / P z) 2 + W.toAffine.a₁ * (P x / P z) * (P y / P z) + W.toAffine.a₃ * (P y / P z) -
        (HPow.hPow (β := ℕ) (P x / P z) 3 + W.toAffine.a₂ * HPow.hPow (β := ℕ) (P x / P z) 2 +
            W.toAffine.a₄ * (P x / P z) +
          W.toAffine.a₆) +
      (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
              W.a₃ * P y / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₄ * P x / P z * 1 +
        W.a₆ * 1)) =
  0
Tactic: rw [eval_polynomial, Affine.evalEval_polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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) 3) =
    Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial
have a : HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 3) +
      (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 + W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * 1 +
              W.a₃ * P y / P z * 1 +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
          W.a₄ * P x / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
        W.a₆ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
    (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial +
      (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
              W.a₃ * P y / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
            W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₄ * P x / P z * 1 +
        W.a₆ * 1)) =
  0
Tactic: linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
    P y ^ 2 / P z ^ 2 * div_self hPz + W.a₁ * P x * P y / P z ^ 2 * div_self hPz
      + W.a₃ * P y / P z * div_self (pow_ne_zero 2 hPz) - W.a₂ * P x ^ 2 / P z ^ 2 * div_self hPz
      - W.a₄ * P x / P z * div_self (pow_ne_zero 2 hPz) - W.a₆ * div_self (pow_ne_zero 3 hPz)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.Equation P ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
have rw : Eq (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) (0 : R) ↔
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0
Tactic: rw [Equation, eval_polynomial, sub_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
⊢ W'.Equation P ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
have rw₁ : HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0 ↔
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0
Tactic: rw [Equation, eval_polynomial, sub_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
rw₁ :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0 ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
⊢ W'.Equation P ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
have rw₂ : HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 =
    HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₆ * HPow.hPow (β := ℕ) (P z) 3 ↔
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 =
    HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₆ * HPow.hPow (β := ℕ) (P z) 3
Tactic: rw [Equation, eval_polynomial, sub_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P_1 : Fin 3 → R
u_1 : R
hu : IsUnit u_1
u : R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.Equation (u • P)
have rw : ∀
  (hP :
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0),
  HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
        W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
      (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
          W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) =
    0
Tactic: rw [equation_iff] at hP ⊢
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P_1 : Fin 3 → R
u_1 : R
hu : IsUnit u_1
u : R
P : Fin 3 → R
hP :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0
⊢ HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
            W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
          (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
              W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) +
        HPow.hPow (β := ℕ) u 3 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 3 *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
    0
have a : HPow.hPow (β := ℕ) (u * P y) 2 * (u * P z) + W'.a₁ * (u * P x) * (u * P y) * (u * P z) +
          W'.a₃ * (u * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
        (HPow.hPow (β := ℕ) (u * P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * (u * P z) +
            W'.a₄ * (u * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 3) +
      HPow.hPow (β := ℕ) u 3 * 0 -
    (0 +
      HPow.hPow (β := ℕ) u 3 *
        (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
  0
Tactic: simp only [smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P_1 : Fin 3 → R
u_1 : R
hu : IsUnit u_1
u : R
P : Fin 3 → R
hP :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0
⊢ HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
        W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
      (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
          W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) =
    0
have a : HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
          W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
        (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
            W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) +
      HPow.hPow (β := ℕ) u 3 * 0 -
    (0 +
      HPow.hPow (β := ℕ) u 3 *
        (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
  0
Tactic: linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) u ^ 3 * hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ W'.Equation P
have h₁ : P = (↑hu.unit⁻¹ : R) • u • P
Tactic: convert! hP (↑hu.unit⁻¹) h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = (↑hu.unit⁻¹ : R) • u • P
have h₁ : P = ((↑hu.unit⁻¹ : R) * u) • P
Tactic: rw [smul_smul, hu.val_inv_mul, one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
h₁ : P = ((↑hu.unit⁻¹ : R) * u) • P
⊢ P = (↑hu.unit⁻¹ : R) • u • P
have h₂ : P = HSMul.hSMul (α := R) 1 P
Tactic: rw [smul_smul, hu.val_inv_mul, one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
h₁ : P = ((↑hu.unit⁻¹ : R) * u) • P
h₂ : P = HSMul.hSMul (α := R) 1 P
⊢ P = (↑hu.unit⁻¹ : R) • u • P
have h₃ : P = P
Tactic: rw [smul_smul, hu.val_inv_mul, one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Equation P ↔ W'.Equation Q
have rcases : ∀ (u : Rˣ), W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation Q
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX =
    W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2)
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
          ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) Y *
        Z -
      ((C : (a : R) → MvPolynomial (Fin 3) R) 3 * HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₂) : MvPolynomial (Fin 3) R) X *
            Z +
        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 2))) =
  W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2)
Tactic: rw [polynomialX_eq]