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'.Δ' : F) ≠ 0
⊢ HMul.hMul (α := F) (-16) 27 ≠ 0 ∧ E'.a₆ ≠ 0

Tactic:
rw [coe_Δ', Δ_of_isShortNF, ha₄', zero_pow three_ne_zero, mul_zero, zero_add, ← mul_assoc,
      mul_ne_zero_iff, pow_ne_zero_iff two_ne_zero] at ha₆'

Premises used: mul_assoc, WeierstrassCurve.Δ_of_isShortNF, zero_add, MulZeroClass.mul_zero, two_ne_zero, WeierstrassCurve.coe_Δ', three_ne_zero, zero_pow, pow_ne_zero_iff, mul_ne_zero_iff
-- 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₆' : HMul.hMul (α := F) (-16) 27 ≠ 0 ∧ E'.a₆ ≠ 0
⊢ E'.a₆ ≠ 0

Tactic:
replace ha₆' := ha₆'.2
-- 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
pos : ∀ (u : F) (hu : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₆ / E'.a₆) 6

Premises used: HDiv.hDiv, IsSepClosed.exists_pow_nat_eq, WeierstrassCurve.a₆, OfNat.ofNat
-- 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 6 = E.a₆ / E'.a₆
rw : E.a₆ ≠ 0 ∧ E'.a₆ ≠ 0
⊢ u ≠ 0

Tactic:
rw [← pow_ne_zero_iff (Nat.succ_ne_zero 5), hu, div_ne_zero_iff]

Premises used: div_ne_zero_iff, Nat.succ_ne_zero, OfNat.ofNat, pow_ne_zero_iff
-- 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 6 = E.a₆ / E'.a₆
⊢ E.a₆ ≠ 0 ∧ E'.a₆ ≠ 0

Tactic:
⟨ha₆, ha₆'⟩

Premises used: And.intro
-- 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 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 6 = E.a₆ / E'.a₆
⊢ u ≠ 0

Tactic:
have hu0 : u ≠ 0 := by
      rw [← pow_ne_zero_iff (Nat.succ_ne_zero 5), hu, 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 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 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 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 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 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 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 [ha₄, ha₄', 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 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (E.a₆ + HMul.hMul (α := F) 0 0 + 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,
        ha₄, Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div, hu]

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 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (E.a₆ + HMul.hMul (α := F) 0 0 + 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_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
pos : ∀ (ha₆ : E.a₆ = 0), ∃ (C : VariableChange F), C • E = E'
neg : ∀ (ha₆ : ¬E.a₆ = 0), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
by_cases ha₆ : E.a₆ = 0

Premises used: WeierstrassCurve.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
⊢ (↑E.Δ' : F) ≠ 0

Tactic:
have ha₄ := E.Δ'.ne_zero
-- 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : (↑E.Δ' : F) ≠ 0
⊢ HMul.hMul (α := F) (-16) 4 ≠ 0 ∧ E.a₄ ≠ 0

Tactic:
rw [coe_Δ', Δ_of_isShortNF, ha₆, zero_pow two_ne_zero, mul_zero, add_zero, ← mul_assoc,
      mul_ne_zero_iff, pow_ne_zero_iff three_ne_zero] at ha₄

Premises used: mul_assoc, WeierstrassCurve.Δ_of_isShortNF, MulZeroClass.mul_zero, two_ne_zero, WeierstrassCurve.coe_Δ', three_ne_zero, add_zero, zero_pow, pow_ne_zero_iff, mul_ne_zero_iff
-- 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : HMul.hMul (α := F) (-16) 4 ≠ 0 ∧ E.a₄ ≠ 0
⊢ E.a₄ ≠ 0

Tactic:
replace ha₄ := ha₄.2
-- 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
⊢ HPow.hPow (β := ℕ) E.a₄ 3 = 0 ∨ HPow.hPow (β := ℕ) E'.a₆ 2 = 0

Tactic:
rw [ha₆, zero_pow two_ne_zero, mul_zero, mul_eq_zero] at heq

Premises used: mul_eq_zero, MulZeroClass.mul_zero, two_ne_zero, zero_pow
-- 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
heq₁ : HPow.hPow (β := ℕ) E.a₄ 3 = 0 ∨ HPow.hPow (β := ℕ) E'.a₆ 2 = 0
⊢ ¬E.a₄ = 0

Tactic:
rw [ha₆, zero_pow two_ne_zero, mul_zero, mul_eq_zero] at heq

Premises used: mul_eq_zero, MulZeroClass.mul_zero, two_ne_zero, zero_pow
-- 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
heq₁ : HPow.hPow (β := ℕ) E.a₄ 3 = 0 ∨ HPow.hPow (β := ℕ) E'.a₆ 2 = 0
ha₅ : ¬E.a₄ = 0
⊢ E.a₆ = 0

Tactic:
rw [ha₆, zero_pow two_ne_zero, mul_zero, mul_eq_zero] at heq

Premises used: mul_eq_zero, MulZeroClass.mul_zero, two_ne_zero, zero_pow