awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
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, ⋯⟩ =
    ![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, ⋯⟩ : Fin 3)
⊢ ((⇑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))

Tactic:
simp only [smul_fin3, comp_fin3]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.comp_fin3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
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, ⋯⟩ =
    ![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, ⋯⟩ : Fin 3)
⊢ ((⇑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))

Tactic:
simp only [smul_fin3, comp_fin3]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.comp_fin3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ 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, ⋯⟩ =
    ![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, ⋯⟩ : Fin 3)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ 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, ⋯⟩ =
    ![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, ⋯⟩ : Fin 3)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ 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, ⋯⟩ =
    ![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, ⋯⟩ : Fin 3)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
F : Type u
inst : CommRing R
inst_1 : Field F
W' : Jacobian R
W : Jacobian F
S : Type s
inst_2 : CommRing S
A : Type u
inst_3 : CommRing A
B : Type v
inst_4 : CommRing B
K : Type v
inst_5 : Field K
x x_1 : R
x_2 : Fin 3 → R
⊢ («x» * x_1) • x_2 = «x» • x_1 • x_2

Tactic:
simp only [smul_fin3, mul_pow, mul_assoc, fin3_def_ext]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, mul_assoc, WeierstrassCurve.Jacobian.fin3_def_ext, mul_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
F : Type u
inst : CommRing R
inst_1 : Field F
W' : Jacobian R
W : Jacobian F
S : Type s
inst_2 : CommRing S
A : Type u
inst_3 : CommRing A
B : Type v
inst_4 : CommRing B
K : Type v
inst_5 : Field K
x : Fin 3 → R
⊢ HSMul.hSMul (α := R) 1 «x» = «x»

Tactic:
simp only [smul_fin3, one_pow, one_mul, fin3_def]

Premises used: one_pow, WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.fin3_def, one_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
hu : IsUnit u
⊢ u • P ≈ P

Tactic:
⟨hu.unit, rfl⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, IsUnit.unit, Set.range, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
hu : IsUnit u
⊢ Eq (α := Quotient (α := Fin 3 → R) (MulAction.orbitRel Rˣ (Fin 3 → R))) ⟦u • P⟧ ⟦P⟧

Tactic:
Quotient.eq.mpr <| smul_equiv P hu

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.smul_equiv, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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⟧
rw₃ rw₄ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
⊢ u • P ≈ v • Q ↔ P ≈ Q

Tactic:
rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]

Premises used: Quotient.eq_iff_equiv, WeierstrassCurve.Jacobian.smul_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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

Tactic:
⟨?_, Quotient.exact.comp <| congrArg _⟩

Premises used: congrArg, Function.comp, Iff.intro, Quotient.exact
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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)
refine : P ≈ Q → P = Q
⊢ P ≈ Q ↔ P = Q

Tactic:
refine ⟨?_, Quotient.exact.comp <| congrArg _⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
simp : HSMul.hSMul (α := R) 1 Q = Q
⊢ (fun (m : Rˣ) ↦ m • Q) u = Q

Tactic:
simp only [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors hQz).mp <| one_mul (Q z) ▸ hz]

Premises used: mul_cancel_right_mem_nonZeroDivisors, Units.smul_def, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
rw rw₁ : Q = Q
⊢ HSMul.hSMul (α := R) 1 Q = Q

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ≠ 0
⊢ P ≈ Q ↔ P = Q

Tactic:
equiv_iff_eq_of_Z_eq' hz <| mem_nonZeroDivisors_of_ne_zero hQz

Premises used: WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq', mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
rcases : ∀ (w : Rˣ), Eq.{r + 1} (α := R) ((fun (m : Rˣ) ↦ m • Q) w z) 0 ↔ Q z = 0
⊢ P z = 0 ↔ Q z = 0

Tactic:
rcases h with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
w : Rˣ
⊢ Eq.{r + 1} (α := R) ((fun (m : Rˣ) ↦ m • Q) w z) 0 ↔ Q z = 0

Tactic:
simp only [Units.smul_def, smul_fin3_ext, Units.mul_right_eq_zero]

Premises used: Units.mul_right_eq_zero, Units.smul_def, WeierstrassCurve.Jacobian.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
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
⊢ P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
simp : HPow.hPow (β := ℕ) (↑u : R) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) ((↑u : R) * Q z) 2
⊢ (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:
simp only [Units.smul_def, smul_fin3_ext]

Premises used: Units.smul_def, WeierstrassCurve.Jacobian.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ HPow.hPow (β := ℕ) (↑u : R) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) ((↑u : R) * Q z) 2

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
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
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
simp : HPow.hPow (β := ℕ) (↑u : R) 3 * Q y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) ((↑u : R) * Q z) 3
⊢ (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:
simp only [Units.smul_def, smul_fin3_ext]

Premises used: Units.smul_def, WeierstrassCurve.Jacobian.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ HPow.hPow (β := ℕ) (↑u : R) 3 * Q y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) ((↑u : R) * Q z) 3

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
hQz : Q z ≠ 0
⊢ ¬P ≈ Q

Tactic:
fun h => hQz <| (Z_eq_zero_of_equiv h).mp hPz

Premises used: WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv, Iff.mp, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hPz : P z ≠ 0
hQz : Q z = 0
⊢ ¬P ≈ Q

Tactic:
fun h => hPz <| (Z_eq_zero_of_equiv h).mpr hQz

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ ¬P ≈ Q

Tactic:
hx.comp X_eq_of_equiv

Premises used: Function.comp, WeierstrassCurve.Jacobian.X_eq_of_equiv, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
⊢ ¬P ≈ Q

Tactic:
hy.comp Y_eq_of_equiv

Premises used: WeierstrassCurve.Jacobian.Y_eq_of_equiv, Function.comp, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
h : (fun (m : Fˣ) ↦ m • Q) (HDiv.hDiv (α := Fˣ) (Units.mk0 (P z) hPz) (Units.mk0 (Q z) hQz)) = P
⊢ P ≈ Q

Tactic:
use Units.mk0 _ hPz / Units.mk0 _ hQz

Premises used: Units.mk0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
⊢ (fun (m : Fˣ) ↦ m • Q) (HDiv.hDiv (α := Fˣ) (Units.mk0 (P z) hPz) (Units.mk0 (Q z) hQz)) = P

Tactic:
simp only [Units.smul_def, smul_fin3, Units.val_div_eq_div_val, Units.val_mk0, div_pow, mul_comm,
    mul_div, ← hx, ← hy, mul_div_cancel_right₀ _ <| pow_ne_zero _ hQz, mul_div_cancel_right₀ _ hQz,
    fin3_def]

Premises used: mul_div, WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.fin3_def, pow_ne_zero, Units.val_div_eq_div_val, mul_div_cancel_right₀, Units.smul_def, div_pow, mul_comm, Units.val_mk0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
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
⊢ 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:
matrix_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
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
⊢ 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

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P x * div_self (pow_ne_zero 2 hPz)

Premises used: pow_ne_zero, OfNat.ofNat, div_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
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
⊢ 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:
matrix_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
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
⊢ 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

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P y * div_self (pow_ne_zero 3 hPz)

Premises used: pow_ne_zero, OfNat.ofNat, div_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ↔
    P x / HPow.hPow (β := ℕ) (P z) 2 = Q x / HPow.hPow (β := ℕ) (Q z) 2

Tactic:
(div_eq_div_iff (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz)).symm

Premises used: pow_ne_zero, div_eq_div_iff, OfNat.ofNat, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3 ↔
    P y / HPow.hPow (β := ℕ) (P z) 3 = Q y / HPow.hPow (β := ℕ) (Q z) 3

Tactic:
(div_eq_div_iff (pow_ne_zero 3 hPz) (pow_ne_zero 3 hQz)).symm

Premises used: pow_ne_zero, div_eq_div_iff, OfNat.ofNat, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
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)
⊢ (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)

Tactic:
rw [polynomial]

Premises used: WeierstrassCurve.Jacobian.polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (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:
simp