awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
⊢ E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0

Tactic:
exact ⟨ha₄, ha₄'⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
⊢ u ≠ 0

Tactic:
have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff four_ne_zero, hu4, div_ne_zero_iff]
    exact ⟨ha₄, ha₄'⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h : HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, 0, 0, 0⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
h₃ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄
h₄ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₆ = E'.a₆
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁

Tactic:
simp [variableChange_a₁]

Premises used: WeierstrassCurve.variableChange_a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂

Tactic:
simp [variableChange_a₂]

Premises used: WeierstrassCurve.variableChange_a₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃

Tactic:
simp [variableChange_a₃]

Premises used: WeierstrassCurve.variableChange_a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (E.a₄ - HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 2 0 * 0 - (0 + HMul.hMul (α := F) 0 0) * 0 +
          3 * HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 2 0 * 0) /
      (E.a₄ / E'.a₄) =
    E'.a₄
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄

Tactic:
simp_rw [variableChange_a₄, a₁_of_isShortNF, a₂_of_isShortNF, a₃_of_isShortNF,
      Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div, hu4]

Premises used: Units.val_inv_eq_inv_val, WeierstrassCurve.a₁_of_isShortNF, inv_mul_eq_div, inv_pow, WeierstrassCurve.variableChange_a₄, WeierstrassCurve.a₃_of_isShortNF, Units.val_mk0, WeierstrassCurve.a₂_of_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (E.a₄ - HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 2 0 * 0 - (0 + HMul.hMul (α := F) 0 0) * 0 +
          3 * HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 2 0 * 0) /
      (E.a₄ / E'.a₄) =
    E'.a₄

Tactic:
simp [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (E.a₆ + 0 * E.a₄ + HPow.hPow (α := F) (β := ℕ) 0 2 * 0 + HPow.hPow (α := F) (β := ℕ) 0 3 - HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 0 0 * 0) /
      (E.a₆ / E'.a₆) =
    E'.a₆
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₆ = E'.a₆

Tactic:
simp_rw [variableChange_a₆, a₁_of_isShortNF, a₂_of_isShortNF, a₃_of_isShortNF,
      Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div, hu6]

Premises used: Units.val_inv_eq_inv_val, WeierstrassCurve.a₁_of_isShortNF, inv_mul_eq_div, inv_pow, WeierstrassCurve.a₃_of_isShortNF, Units.val_mk0, WeierstrassCurve.a₂_of_isShortNF, WeierstrassCurve.variableChange_a₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (E.a₆ + 0 * E.a₄ + HPow.hPow (α := F) (β := ℕ) 0 2 * 0 + HPow.hPow (α := F) (β := ℕ) 0 3 - HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 0 0 * 0) /
      (E.a₆ / E'.a₆) =
    E'.a₆

Tactic:
simp [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
obtain : ∀ (p : ℕ), CharP F p → ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨p, _⟩ := CharP.exists F

Premises used: CharP.exists
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h : CharP F p
pos : ∀ (hchar2 : p = 2), ∃ (C : VariableChange F), C • E = E'
neg : ∀ (hchar2 : ¬p = 2), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
by_cases hchar2 : p = 2
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : p = 2
⊢ CharP F 2

Tactic:
subst hchar2
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
h : CharP F 2
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exists_variableChange_of_char_two _ _ heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
h : CharP F 2
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exact exists_variableChange_of_char_two _ _ heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : ¬p = 2
pos : ∀ (hchar3 : p = 3), ∃ (C : VariableChange F), C • E = E'
neg : ∀ (hchar3 : ¬p = 3), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
by_cases hchar3 : p = 3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : ¬p = 2
hchar3 : p = 3
⊢ CharP F 3

Tactic:
subst hchar3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h_1 : CharP F p
hchar2 : ¬p = 2
hchar3 : p = 3
h : CharP F 3
⊢ ¬Eq (α := ℕ) 3 2

Tactic:
subst hchar3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
h : CharP F 3
hchar2 : ¬Eq (α := ℕ) 3 2
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exists_variableChange_of_char_three _ _ heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
h : CharP F 3
hchar2 : ¬Eq (α := ℕ) 3 2
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exact exists_variableChange_of_char_three _ _ heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : ¬p = 2
hchar3 : ¬p = 3
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exists_variableChange_of_char_ne_two_or_three _ _ hchar2 hchar3 heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_ne_two_or_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : ¬p = 2
hchar3 : ¬p = 3
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exact exists_variableChange_of_char_ne_two_or_three _ _ hchar2 hchar3 heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_ne_two_or_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
P : Fin 3 → R
h : ∀ (n : Fin (Nat.succ 0).succ.succ), ![P x, P y, P z] n = P n
⊢ ![P x, P y, P z] = P

Tactic:
ext n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
h :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h₂ :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ ![P x, P y, P z] n = P n

Tactic:
fin_cases n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
a b c : R
⊢ ![a, b, c] x = a ∧ ![a, b, c] y = b ∧ ![a, b, c] z = c

Tactic:
⟨rfl, rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
S : Type s
f : R → S
a b c : R
⊢ f ∘ ![a, b, c] = ![f a, f b, f c]

Tactic:
(FinVec.map_eq ..).symm

Premises used: Eq.mpr, FinVec.map, Fin.cons, Fin.induction.go, Fin.induction, FinVec.map_eq, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
⊢ u • P = ![HPow.hPow (β := ℕ) u 2 * P x, HPow.hPow (β := ℕ) u 3 * P y, u * P z]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
⊢ (u • P) x = HPow.hPow (β := ℕ) u 2 * P x ∧ (u • P) y = HPow.hPow (β := ℕ) u 3 * P y ∧ (u • P) z = u * P z

Tactic:
⟨rfl, rfl, rfl⟩

Premises used: And.intro, rfl
-- 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 :
  ∀ (n : Fin 3),
    ((⇑f : (a : R) → S) ∘ (u • P)) n =
      HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) n
⊢ (⇑f : (a : R) → S) ∘ (u • P) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)

Tactic:
ext n
-- 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
n : Fin 3
h :
  ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))
h₁ :
  ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))
h₂ :
  ((⇑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))
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) n =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) n

Tactic:
fin_cases n
-- 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)] ⟨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)
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
      ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))

Tactic:
simp only [smul_fin3, comp_fin3]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.comp_fin3