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

Tactic:
(pow_eq_zero_iff two_ne_zero).1 <| heq.resolve_left <| pow_ne_zero 3 ha₄

Premises used: pow_eq_zero_iff, pow_ne_zero, Or.resolve_left, two_ne_zero, Iff.mp, 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 = 0 ∨ HPow.hPow (β := ℕ) E'.a₆ 2 = 0
ha₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
⊢ E'.a₆ = 0

Tactic:
exact (pow_eq_zero_iff two_ne_zero).1 <| heq.resolve_left <| pow_ne_zero 3 ha₄

Premises used: pow_eq_zero_iff, pow_ne_zero, Or.resolve_left, two_ne_zero, Iff.mp, 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
⊢ E'.a₆ = 0

Tactic:
have ha₆' : E'.a₆ = 0 := by
      rw [ha₆, zero_pow two_ne_zero, mul_zero, mul_eq_zero] at heq
      exact (pow_eq_zero_iff two_ne_zero).1 <| heq.resolve_left <| pow_ne_zero 3 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
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.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₄ : 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
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
pos : ∀ (u : F) (hu : HPow.hPow (β := ℕ) u 4 = 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₄) 4

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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
rw : E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0
⊢ u ≠ 0

Tactic:
rw [← pow_ne_zero_iff four_ne_zero, hu, div_ne_zero_iff]

Premises used: four_ne_zero, div_ne_zero_iff, 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
⊢ u ≠ 0

Tactic:
have hu0 : u ≠ 0 := by
      rw [← pow_ne_zero_iff four_ne_zero, 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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, hu]

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₄_1 : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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 : 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
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 4 = 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
h : E'.a₄ = 0
⊢ E.a₄ = 0 ∨ E'.a₆ = 0

Tactic:
rw [h, zero_pow three_ne_zero, zero_mul, mul_eq_zero,
      pow_eq_zero_iff two_ne_zero, pow_eq_zero_iff three_ne_zero] at heq

Premises used: pow_eq_zero_iff, MulZeroClass.zero_mul, mul_eq_zero, two_ne_zero, three_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_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
h : E'.a₄ = 0
heq₁ : E.a₄ = 0 ∨ E'.a₆ = 0
⊢ ¬E.a₄ = 0

Tactic:
rw [h, zero_pow three_ne_zero, zero_mul, mul_eq_zero,
      pow_eq_zero_iff two_ne_zero, pow_eq_zero_iff three_ne_zero] at heq

Premises used: pow_eq_zero_iff, MulZeroClass.zero_mul, mul_eq_zero, two_ne_zero, three_ne_zero, zero_pow