awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 *
          (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
        Q x,
      HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
          (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
        Q y,
      0] =
    P
⊢ (fun (m : Fˣ) ↦ m • Q) (hPy.unit / hPx.unit * (hQx.unit / hQy.unit)) = P

Tactic:
simp only [Units.smul_def, smul_fin3, Units.val_mul, Units.val_div_eq_div_val, IsUnit.unit_spec,
    mul_pow, div_pow, hQz, mul_zero]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, Units.val_div_eq_div_val, MulZeroClass.mul_zero, Units.smul_def, div_pow, mul_pow, IsUnit.unit_spec, Units.val_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
rw : ![P x, P y, 0]
| P

Tactic:
rw [← fin3_def P, hPz]

Premises used: WeierstrassCurve.Jacobian.fin3_def
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 *
          (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
        Q x,
      HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
          (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
        Q y,
      0] =
    ![P x, P y, 0]
⊢ ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 *
          (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
        Q x,
      HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
          (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
        Q y,
      0] =
    P

Tactic:
conv_rhs => rw [← fin3_def P, hPz]

Premises used: WeierstrassCurve.Jacobian.fin3_def
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₁ :
  HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
⊢ ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 *
          (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
        Q x,
      HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
          (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
        Q y,
      0] =
    ![P x, P y, 0]

Tactic:
congr! 2
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₁ :
  HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 *
        (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₂ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) * Q x = P x
h₃ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q x) 3) * Q x = P x
h₄ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / (HPow.hPow (β := ℕ) (Q x) 2 * Q x)) * Q x = P x
h₅ : P x * (Q x)⁻¹ * Q x = P x
h₆ h₇ : P x = P x
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x

Tactic:
rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]

Premises used: IsUnit.mul_div_cancel_left, pow_succ, IsUnit.pow, And.left, IsUnit.div_mul_cancel_left, OfNat.ofNat, IsUnit.inv_mul_cancel_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P y) 2 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
h₁ :
  HPow.hPow (β := ℕ) (P y) 2 * P y / HPow.hPow (β := ℕ) (P y) 2 *
        (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
h₂ : P y * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) * Q y = P y
h₃ : P y * (HPow.hPow (β := ℕ) (Q y) 2 / HPow.hPow (β := ℕ) (Q y) 3) * Q y = P y
h₄ : P y * (HPow.hPow (β := ℕ) (Q y) 2 / (HPow.hPow (β := ℕ) (Q y) 2 * Q y)) * Q y = P y
h₅ : P y * (Q y)⁻¹ * Q y = P y
h₆ h₇ : P y = P y
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y

Tactic:
rw [← hP.left, pow_succ, (hPy.pow 2).mul_div_cancel_left, ← hQ.left, pow_succ _ 2,
      (hQy.pow 2).div_mul_cancel_left, hQy.inv_mul_cancel_right]

Premises used: IsUnit.mul_div_cancel_left, pow_succ, IsUnit.pow, And.left, IsUnit.div_mul_cancel_left, OfNat.ofNat, IsUnit.inv_mul_cancel_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ P ≈ ![1, 1, 0]

Tactic:
equiv_of_Z_eq_zero hP nonsingular_zero hPz rfl

Premises used: WeierstrassCurve.Jacobian.nonsingular_zero, WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) ↔ P ≈ Q

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
refine_1 :
  ∀ (h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)), P ≈ Q
refine_2 :
  ∀ (h : P ≈ Q), HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) ↔ P ≈ Q

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
pos : ∀ (hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
neg : ∀ (hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
⊢ P ≈ Q

Tactic:
by_cases hz : f (P z) = 0

Premises used: OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ P ≈ Q

Tactic:
equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
        (map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz

Premises used: WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv, RingHom.injective, map_eq_zero_iff, Iff.mp, WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ P ≈ Q

Tactic:
exact equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
        (map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz

Premises used: WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv, RingHom.injective, map_eq_zero_iff, Iff.mp, WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ P ≈ Q

Tactic:
equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
        ((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv, Function.comp, RingHom.injective, Iff.mp, WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq, map_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
neg₁ : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
⊢ P ≈ Q

Tactic:
refine equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
        ((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv, Function.comp, RingHom.injective, Iff.mp, WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq, map_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg :
  Eq.{v + 1} (α := K) ((f : (a : F) → K) (P x * HPow.hPow (β := ℕ) (Q z) 2) : K)
    ((f : (a : F) → K) (Q x * HPow.hPow (β := ℕ) (P z) 2) : K)
⊢ P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2

Tactic:
apply f.injective

Premises used: RingHom.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg :
  HMul.hMul (α := K) ((f : (a : F) → K) (P x) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (Q z) : K) 2) =
    HMul.hMul (α := K) ((f : (a : F) → K) (Q x) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (P z) : K) 2)
⊢ Eq.{v + 1} (α := K) ((f : (a : F) → K) (P x * HPow.hPow (β := ℕ) (Q z) 2) : K)
    ((f : (a : F) → K) (Q x * HPow.hPow (β := ℕ) (P z) 2) : K)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg :
  Eq.{v + 1} (α := K) ((f : (a : F) → K) (P y * HPow.hPow (β := ℕ) (Q z) 3) : K)
    ((f : (a : F) → K) (Q y * HPow.hPow (β := ℕ) (P z) 3) : K)
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3

Tactic:
apply f.injective

Premises used: RingHom.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg :
  HMul.hMul (α := K) ((f : (a : F) → K) (P y) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (Q z) : K) 3) =
    HMul.hMul (α := K) ((f : (a : F) → K) (Q y) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (P z) : K) 3)
⊢ Eq.{v + 1} (α := K) ((f : (a : F) → K) (P y * HPow.hPow (β := ℕ) (Q z) 3) : K)
    ((f : (a : F) → K) (Q y * HPow.hPow (β := ℕ) (P z) 3) : K)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ HMul.hMul (α := K) ((f : (a : F) → K) (P x) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (Q z) : K) 2) =
    HMul.hMul (α := K) ((f : (a : F) → K) (Q x) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (P z) : K) 2)

Tactic:
X_eq_of_equiv h

Premises used: WeierstrassCurve.Jacobian.X_eq_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ HMul.hMul (α := K) ((f : (a : F) → K) (P y) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (Q z) : K) 3) =
    HMul.hMul (α := K) ((f : (a : F) → K) (Q y) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (P z) : K) 3)

Tactic:
Y_eq_of_equiv h

Premises used: WeierstrassCurve.Jacobian.Y_eq_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ HMul.hMul (α := K) ((f : (a : F) → K) (P x) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (Q z) : K) 2) =
    HMul.hMul (α := K) ((f : (a : F) → K) (Q x) : K) (HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) (P z) : K) 2)

Tactic:
exacts [X_eq_of_equiv h, Y_eq_of_equiv h]

Premises used: WeierstrassCurve.Jacobian.Y_eq_of_equiv, WeierstrassCurve.Jacobian.X_eq_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
refine_2 :
  ∀ (u : Fˣ) (hP : W.Nonsingular ((fun (m : Fˣ) ↦ m • Q) u)),
    HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K)
      (Function.comp.{1, u + 1, v + 1} (β := F) (⇑f : (a : F) → K) ((fun (m : Fˣ) ↦ m • Q) u)) ((⇑f : (a : F) → K) ∘ Q)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
Q : Fin 3 → F
hQ : W.Nonsingular Q
u : Fˣ
hP : W.Nonsingular ((fun (m : Fˣ) ↦ m • Q) u)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K)
    (Function.comp.{1, u + 1, v + 1} (β := F) (⇑f : (a : F) → K) ((fun (m : Fˣ) ↦ m • Q) u)) ((⇑f : (a : F) → K) ∘ Q)

Tactic:
⟨Units.map f u, (comp_smul ..).symm⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, Set.range, DFunLike.coe, Units.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
K : Type v
inst_1 : Field K
f : F →+* K
Q : Fin 3 → F
hQ : W.Nonsingular Q
u : Fˣ
hP : W.Nonsingular ((fun (m : Fˣ) ↦ m • Q) u)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K)
    (Function.comp.{1, u + 1, v + 1} (β := F) (⇑f : (a : F) → K) ((fun (m : Fˣ) ↦ m • Q) u)) ((⇑f : (a : F) → K) ∘ Q)

Tactic:
exact ⟨Units.map f u, (comp_smul ..).symm⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P

Tactic:
Iff.rfl

Premises used: Iff.rfl, WeierstrassCurve.Jacobian.NonsingularLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
⊢ W'.NonsingularLift ⟦![1, 1, 0]⟧

Tactic:
nonsingular_zero

Premises used: WeierstrassCurve.Jacobian.NonsingularLift, WeierstrassCurve.Jacobian.nonsingular_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
a b : R
⊢ W'.NonsingularLift ⟦![a, b, 1]⟧ ↔ W'.toAffine.Nonsingular a b

Tactic:
nonsingular_some a b

Premises used: WeierstrassCurve.Jacobian.NonsingularLift, WeierstrassCurve.Jacobian.nonsingular_some
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» y) 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) S) (β := MvPolynomial (Fin 3) S)
                ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₁ : MvPolynomial (Fin 3) S) («X» x) *
              «X» y *
            «X» z +
        HMul.hMul (α := MvPolynomial (Fin 3) S) (β := MvPolynomial (Fin 3) S)
            ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₃ : MvPolynomial (Fin 3) S) («X» y) *
          HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» z) 3 -
      (HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» x) 3 +
            HMul.hMul (α := MvPolynomial (Fin 3) S)
                ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₂ : MvPolynomial (Fin 3) S)
                (HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» x) 2) *
              HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» z) 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) S) (β := MvPolynomial (Fin 3) S)
              ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₄ : MvPolynomial (Fin 3) S) («X» x) *
            HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» z) 4 +
        HMul.hMul (α := MvPolynomial (Fin 3) S)
          ((C : (a : S) → MvPolynomial (Fin 3) S) (W'.map f).a₆ : MvPolynomial (Fin 3) S)
          (HPow.hPow (α := MvPolynomial (Fin 3) S) (β := ℕ) («X» z) 6)) =
    ((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      (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)))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S)
        (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
              (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
            W'.polynomial :
          MvPolynomial (Fin 3) S) :
      S)
    (0 : S)
rw₂ : eval₂ f ((⇑f : (a : R) → S) ∘ P) W'.polynomial = 0
rw₃ :
  Eq.{s + 1} (α := S) ((f : (a : R) → S) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) : S) (0 : S)
rw₄ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
rw₅ rw₆ : Eq.{s + 1} (α := S) 0 0
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)

Tactic:
rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]

Premises used: MvPolynomial.eval_map, map_zero, WeierstrassCurve.Jacobian.Equation, WeierstrassCurve.Jacobian.map_polynomial, MvPolynomial.eval₂_comp