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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ -HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆ = -HPow.hPow (β := ℕ) E'.a₂ 3 * E.a₆

Tactic:
simp_rw [j_of_isCharThreeJNeZeroNF_of_char_three, div_eq_div_iff ha₆ ha₆'] at heq

Premises used: div_eq_div_iff, WeierstrassCurve.j_of_isCharThreeJNeZeroNF_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
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
heq : -HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆ = -HPow.hPow (β := ℕ) E'.a₂ 3 * E.a₆
h :
  (E.a₆ + HMul.hMul (α := F) 0 0 + HPow.hPow (α := F) (β := ℕ) 0 2 * E.a₂ + HPow.hPow (α := F) (β := ℕ) 0 3 -
            HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 0 0 * 0) /
      HPow.hPow (β := ℕ) (E.a₂ / E'.a₂) 3 =
    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_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF,
      a₄_of_isCharThreeJNeZeroNF, Units.val_inv_eq_inv_val, Units.val_mk0,
      inv_pow, inv_mul_eq_div, pow_mul u 2 3, hu]

Premises used: WeierstrassCurve.a₃_of_isCharThreeJNeZeroNF, Units.val_inv_eq_inv_val, inv_mul_eq_div, WeierstrassCurve.a₄_of_isCharThreeJNeZeroNF, inv_pow, pow_mul, Units.val_mk0, WeierstrassCurve.a₁_of_isCharThreeJNeZeroNF, OfNat.ofNat, WeierstrassCurve.variableChange_a₆
-- 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
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
heq : -HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆ = -HPow.hPow (β := ℕ) E'.a₂ 3 * E.a₆
h : E.a₆ * HPow.hPow (β := ℕ) E'.a₂ 3 = HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆
⊢ (E.a₆ + HMul.hMul (α := F) 0 0 + HPow.hPow (α := F) (β := ℕ) 0 2 * E.a₂ + HPow.hPow (α := F) (β := ℕ) 0 3 -
            HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 0 0 * 0) /
      HPow.hPow (β := ℕ) (E.a₂ / E'.a₂) 3 =
    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
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
heq : -HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆ = -HPow.hPow (β := ℕ) E'.a₂ 3 * E.a₆
⊢ E.a₆ * HPow.hPow (β := ℕ) E'.a₂ 3 = HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆

Tactic:
linear_combination heq
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
⊢ (↑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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : (↑E.Δ' : F) ≠ 0
⊢ E.a₄ ≠ 0

Tactic:
rw [E.coe_Δ', Δ_of_isShortNF_of_char_three, neg_ne_zero, pow_ne_zero_iff three_ne_zero] at ha₄

Premises used: WeierstrassCurve.Δ_of_isShortNF_of_char_three, WeierstrassCurve.coe_Δ', neg_ne_zero, three_ne_zero, pow_ne_zero_iff
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : (↑E'.Δ' : F) ≠ 0
⊢ E'.a₄ ≠ 0

Tactic:
rw [E'.coe_Δ', Δ_of_isShortNF_of_char_three, neg_ne_zero, pow_ne_zero_iff three_ne_zero] at ha₄'

Premises used: WeierstrassCurve.Δ_of_isShortNF_of_char_three, WeierstrassCurve.coe_Δ', neg_ne_zero, three_ne_zero, pow_ne_zero_iff
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ Eq.{u_1 + 1} (α := F) 4 1

Tactic:
linear_combination CharP.cast_eq_zero F 3

Premises used: CharP.cast_eq_zero, OfNat.ofNat
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
rw : Ne.{u_1 + 1} (α := F) 1 0
⊢ Ne.{u_1 + 1} (α := F) 4 0

Tactic:
rw [show (4 : F) = 1 by linear_combination CharP.cast_eq_zero F 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ NeZero.{u_1} (R := F) 4

Tactic:
haveI : NeZero (4 : F) := NeZero.mk <| by
    rw [show (4 : F) = 1 by linear_combination CharP.cast_eq_zero F 3]
    exact one_ne_zero
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
obtain : ∀ (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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
⊢ Dvd.dvd (α := ℕ) 3 3

Tactic:
simp
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
⊢ LE.le (α := ℕ) 2 3

Tactic:
simp
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
obtain :
  ∀ (r : F) (hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0),
    ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨r, hr⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 3 3
    1 _ (E.a₆ - u ^ 6 * E'.a₆) (by simp) (by simp) ha₄

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, WeierstrassCurve.a₆, IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C', OfNat.ofNat
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
⊢ 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
⊢ 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
⊢ 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h : HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, r, 0, 0⟩
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
h₃ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄
h₄ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₆ = E'.a₆
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h : (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) * (0 + HMul.hMul (α := F) 2 0) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁

Tactic:
simp_rw [variableChange_a₁, a₁_of_isShortNF]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.a₁_of_isShortNF
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) * (0 + HMul.hMul (α := F) 2 0) = 0

Tactic:
ring1
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 2 *
      (0 - HMul.hMul (α := F) 0 0 + 0 * r - HPow.hPow (α := F) (β := ℕ) 0 2) =
    0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂

Tactic:
simp_rw [variableChange_a₂, a₁_of_isShortNF, a₂_of_isShortNF,
      show (3 : F) = 0 from CharP.cast_eq_zero F 3]

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₁_of_isShortNF, WeierstrassCurve.variableChange_a₂, OfNat.ofNat, WeierstrassCurve.a₂_of_isShortNF
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 2 *
      (0 - HMul.hMul (α := F) 0 0 + 0 * r - HPow.hPow (α := F) (β := ℕ) 0 2) =
    0

Tactic:
ring1
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h : HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 3 * (0 + r * 0 + HMul.hMul (α := F) 2 0) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, a₁_of_isShortNF, a₃_of_isShortNF]

Premises used: WeierstrassCurve.a₁_of_isShortNF, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.a₃_of_isShortNF
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 3 * (0 + r * 0 + HMul.hMul (α := F) 2 0) = 0

Tactic:
ring1
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  (E.a₄ - HMul.hMul (α := F) 0 0 + 2 * r * 0 - (0 + r * 0) * 0 + 0 * HPow.hPow (β := ℕ) r 2 -
        HMul.hMul (α := F) 2 0 * 0) /
      (E.a₄ / E'.a₄) =
    E'.a₄
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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,
      show (3 : F) = 0 from CharP.cast_eq_zero F 3]

Premises used: CharP.cast_eq_zero, 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, OfNat.ofNat, WeierstrassCurve.a₂_of_isShortNF
-- 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.a₄ - HMul.hMul (α := F) 0 0 + 2 * r * 0 - (0 + r * 0) * 0 + 0 * HPow.hPow (β := ℕ) r 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  (E.a₆ + r * E.a₄ + HPow.hPow (β := ℕ) r 2 * 0 + HPow.hPow (β := ℕ) r 3 - HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        r * 0 * 0) /
      HPow.hPow (β := ℕ) u 6 =
    E'.a₆
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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]

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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h : E.a₆ + r * E.a₄ + HPow.hPow (β := ℕ) r 3 = HPow.hPow (β := ℕ) u 6 * E'.a₆
⊢ (E.a₆ + r * E.a₄ + HPow.hPow (β := ℕ) r 2 * 0 + HPow.hPow (β := ℕ) r 3 - HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        r * 0 * 0) /
      HPow.hPow (β := ℕ) u 6 =
    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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ E.a₆ + r * E.a₄ + HPow.hPow (β := ℕ) r 3 = HPow.hPow (β := ℕ) u 6 * E'.a₆

Tactic:
linear_combination hr
-- 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
inst_4 : CharP F 3
heq : E.j = E'.j
of_j_ne_zero : ∀ (C : VariableChange F) [(C • E).IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
of_j_eq_zero : ∀ (C : VariableChange F) [(C • E).IsShortNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharThreeNF

Premises used: Polynomial.C, WeierstrassCurve.exists_variableChange_isCharThreeNF
-- 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
inst_4 : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
of_j_ne_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
of_j_ne_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsShortNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF

Premises used: WeierstrassCurve.exists_variableChange_isCharThreeNF