awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
have h₆ : P 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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)
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
have 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
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
have 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
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
have h₂ : P y * (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
have h₃ : P y * (HPow.hPow (β := ℕ) (Q y) 2 / 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
have h₄ : P y * (HPow.hPow (β := ℕ) (Q y) 2 / (HPow.hPow (β := ℕ) (Q y) 2 * Q y)) * 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
have h₅ : P y * (Q y)⁻¹ * 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y =
    P y
have h₆ : P 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
have 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
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) ↔ P ≈ Q
have 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)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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)
⊢ P ≈ Q
have pos : ∀ (hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
Tactic: by_cases hz : f (P z) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ P ≈ Q
have neg : ∀ (hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
Tactic: by_cases hz : f (P z) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
have neg : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
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) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ P ≈ Q
have neg₁ : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
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) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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 x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
have 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)
Tactic: apply f.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: map_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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 y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
have 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)
Tactic: apply f.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: map_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
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
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
have 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)
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, hP, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
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)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have 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)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
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)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₂ : eval₂ f ((⇑f : (a : R) → S) ∘ P) W'.polynomial = 0
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
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
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₃ : Eq.{s + 1} (α := S) ((f : (a : R) → S) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) : S) (0 : S)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
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)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₄ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
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)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₅ : Eq.{s + 1} (α := S) 0 0
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomial)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial ((W'⁄A).map (↑f : A →+* B)).polynomial
Tactic: rw [← map_polynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial ((W'⁄A).map (↑f : A →+* B)).polynomial
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomial)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial (W'⁄B).polynomial
Tactic: rw [← map_polynomial, map_baseChange]