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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.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_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
hE' : (C • E').IsShortNF
heq₁ : E.j = (C • E').j
⊢ (C • E').IsShortNF

Tactic:
rw [← variableChange_j E' C] at heq

Premises used: WeierstrassCurve.variableChange_j
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.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_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
inr : ∀ (C' : VariableChange F) (hC : C' • E = C • E'), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C', hC⟩ := this _ heq hE'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.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_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
rw : C⁻¹ • C' • E = E'
rw₁ : C⁻¹ • C • E' = E'
rw₂ : (C⁻¹ * C) • E' = E'
rw₃ : HSMul.hSMul (α := VariableChange F) 1 E' = E'
rw₄ rw₅ : E' = E'
⊢ (C⁻¹ * C') • E = E'

Tactic:
rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

Premises used: inv_mul_cancel, one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.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_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exact ⟨C⁻¹ * C', by rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]⟩
-- 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
heq : E.j = E'.j
h_1 : E'.IsShortNF
⊢ HPow.hPow (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))

Tactic:
simp_rw [j, Units.val_inv_eq_inv_val, inv_mul_eq_div,
    div_eq_div_iff E.Δ'.ne_zero E'.Δ'.ne_zero, coe_Δ', Δ_of_isShortNF, c₄_of_isShortNF] at heq

Premises used: WeierstrassCurve.j, Units.val_inv_eq_inv_val, inv_mul_eq_div, WeierstrassCurve.Δ_of_isShortNF, Units.ne_zero, WeierstrassCurve.Δ', div_eq_div_iff, WeierstrassCurve.c₄_of_isShortNF, WeierstrassCurve.coe_Δ'
-- 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
⊢ HPow.hPow (α := F) (β := ℕ) 2 16 * HPow.hPow (α := F) (β := ℕ) 3 6 ≠ 0

Tactic:
have := mul_ne_zero (pow_ne_zero 16 hchar2) (pow_ne_zero 6 hchar3)
-- 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_5 : 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
this : HPow.hPow (α := F) (β := ℕ) 2 16 * HPow.hPow (α := F) (β := ℕ) 3 6 ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 47775744 0

Tactic:
norm_num1 at this
-- 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_5 : 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
this : Ne.{u_1 + 1} (α := F) 47775744 0
⊢ Ne.{u_1 + 1} (α := F) 47775744 0

Tactic:
this
-- 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_5 : 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
this : Ne.{u_1 + 1} (α := F) 47775744 0
⊢ Ne.{u_1 + 1} (α := F) 47775744 0

Tactic:
exact this
-- 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_5 : 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
this : Invertible (α := F) 47775744 := invertibleOfNonzero ⋯
rw :
  47775744 * (HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2) =
    47775744 * (HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2)
⊢ HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2

Tactic:
rw [← mul_right_inj_of_invertible (47775744 : F)]

Premises used: mul_right_inj_of_invertible, 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_5 : 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
this : Invertible (α := F) 47775744 := invertibleOfNonzero ⋯
⊢ 47775744 * (HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2) =
    47775744 * (HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2)

Tactic:
linear_combination heq
-- 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
⊢ HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2

Tactic:
replace heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2 := by
    letI : Invertible (47775744 : F) := invertibleOfNonzero <| by
      have := mul_ne_zero (pow_ne_zero 16 hchar2) (pow_ne_zero 6 hchar3)
      norm_num1 at this
      exact this
    rw [← mul_right_inj_of_invertible (47775744 : F)]
    linear_combination heq
-- 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
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
⊢ (↑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₄ : 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₆ : 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
⊢ HPow.hPow (β := ℕ) E'.a₄ 3 = 0 ∨ HPow.hPow (β := ℕ) E.a₆ 2 = 0

Tactic:
rw [ha₄, zero_pow three_ne_zero, zero_mul, zero_eq_mul] at heq

Premises used: MulZeroClass.zero_mul, zero_eq_mul, 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 : 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
heq₁ : HPow.hPow (β := ℕ) E'.a₄ 3 = 0 ∨ HPow.hPow (β := ℕ) E.a₆ 2 = 0
⊢ E.a₄ = 0

Tactic:
rw [ha₄, zero_pow three_ne_zero, zero_mul, zero_eq_mul] at heq

Premises used: MulZeroClass.zero_mul, zero_eq_mul, 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 : 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
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 three_ne_zero, zero_mul, zero_eq_mul] at heq

Premises used: MulZeroClass.zero_mul, zero_eq_mul, 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 : 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₄ : E.a₄ = 0
ha₆ : E.a₆ ≠ 0
⊢ E'.a₄ = 0

Tactic:
(pow_eq_zero_iff three_ne_zero).1 <| heq.resolve_right <| pow_ne_zero 2 ha₆

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

Tactic:
exact (pow_eq_zero_iff three_ne_zero).1 <| heq.resolve_right <| pow_ne_zero 2 ha₆

Premises used: pow_eq_zero_iff, pow_ne_zero, Iff.mp, Or.resolve_right, three_ne_zero, 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
⊢ E'.a₄ = 0

Tactic:
have ha₄' : E'.a₄ = 0 := by
      rw [ha₄, zero_pow three_ne_zero, zero_mul, zero_eq_mul] at heq
      exact (pow_eq_zero_iff three_ne_zero).1 <| heq.resolve_right <| pow_ne_zero 2 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
⊢ (↑E'.Δ' : F) ≠ 0

Tactic:
have ha₆' := E'.Δ'.ne_zero