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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
obtain : ∀ (u : F) (hu : HPow.hPow (β := ℕ) u 3 = 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₃) 3

Premises used: HDiv.hDiv, WeierstrassCurve.a₃, IsSepClosed.exists_pow_nat_eq, 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
⊢ Dvd.dvd (α := ℕ) 2 4

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

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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
obtain :
  ∀ (s : F) (hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0),
    ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨s, hs⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 4
    1 _ (E.a₄ - u ^ 4 * 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
⊢ Dvd.dvd (α := ℕ) 2 2

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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
⊢ LE.le (α := ℕ) 2 2

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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
obtain :
  ∀ (t : F)
    (ht :
      1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
          (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
        0),
    ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨t, ht⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 2
    1 _ (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) (by simp) (by simp) ha₃

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, HAdd.hAdd, WeierstrassCurve.a₆, 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
rw : E.a₃ ≠ 0 ∧ E'.a₃ ≠ 0
⊢ u ≠ 0

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

Premises used: div_ne_zero_iff, 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
⊢ u ≠ 0

Tactic:
have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff three_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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
h :
  HSMul.hSMul (α := VariableChange F)
      { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E =
    E'
⊢ ∃ (C : VariableChange F), C • E = E'

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

Tactic:
simp_rw [variableChange_a₁, a₁_of_isCharTwoJEqZeroNF,
      show (2 : F) = 0 from CharP.cast_eq_zero F 2]

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

Tactic:
linear_combination CharP.cast_eq_zero F 2

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

Tactic:
simp_rw [variableChange_a₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF,
      show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]

Premises used: WeierstrassCurve.variableChange_a₂, WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF, WeierstrassCurve.a₂_of_isCharTwoJEqZeroNF
-- 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
⊢ HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 2 *
      (0 - s * 0 + 1 * HPow.hPow (β := ℕ) s 2 - HPow.hPow (β := ℕ) s 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
h : (E.a₃ + HPow.hPow (β := ℕ) s 2 * 0 + 0 * t) / (E.a₃ / E'.a₃) = E'.a₃
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₃ =
    E'.a₃

Tactic:
simp_rw [variableChange_a₃, Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div,
      hu, a₁_of_isCharTwoJEqZeroNF, show (2 : F) = 0 from CharP.cast_eq_zero F 2]

Premises used: CharP.cast_eq_zero, Units.val_inv_eq_inv_val, inv_mul_eq_div, WeierstrassCurve.variableChange_a₃, inv_pow, WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF, Units.val_mk0, 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
⊢ (E.a₃ + HPow.hPow (β := ℕ) s 2 * 0 + 0 * t) / (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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
h : E.a₄ - s * E.a₃ + HPow.hPow (β := ℕ) s 4 * 3 - s * 2 * t = HPow.hPow (β := ℕ) u 4 * E'.a₄
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₄ =
    E'.a₄

Tactic:
simp [field, variableChange_a₄, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]

Premises used: WeierstrassCurve.variableChange_a₄, WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF, WeierstrassCurve.a₂_of_isCharTwoJEqZeroNF
-- 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
⊢ E.a₄ - s * E.a₃ + HPow.hPow (β := ℕ) s 4 * 3 - s * 2 * t = HPow.hPow (β := ℕ) u 4 * E'.a₄

Tactic:
linear_combination hs + (s ^ 4 - s * t - E.a₃ * s) * CharP.cast_eq_zero F 2

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, WeierstrassCurve.a₃, HPow.hPow, 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
h :
  E.a₆ + HPow.hPow (β := ℕ) s 2 * E.a₄ + HPow.hPow (β := ℕ) s 6 - t * E.a₃ - HPow.hPow (β := ℕ) t 2 =
    HPow.hPow (β := ℕ) u 6 * E'.a₆
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₆ =
    E'.a₆

Tactic:
simp [field, variableChange_a₆, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]

Premises used: WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF, WeierstrassCurve.a₂_of_isCharTwoJEqZeroNF, 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 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero.{u_1} (R := F) 3
u : F
hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃
s : F
hs : 1 * HPow.hPow (β := ℕ) s 4 + E.a₃ * s + (E.a₄ - HPow.hPow (β := ℕ) u 4 * E'.a₄) = 0
t : F
ht :
  1 * HPow.hPow (β := ℕ) t 2 + E.a₃ * t +
      (HPow.hPow (β := ℕ) s 6 + E.a₄ * HPow.hPow (β := ℕ) s 2 + E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) =
    0
hu0 : u ≠ 0
⊢ E.a₆ + HPow.hPow (β := ℕ) s 2 * E.a₄ + HPow.hPow (β := ℕ) s 6 - t * E.a₃ - HPow.hPow (β := ℕ) t 2 =
    HPow.hPow (β := ℕ) u 6 * E'.a₆

Tactic:
linear_combination ht - (t ^ 2 + E.a₃ * t) * CharP.cast_eq_zero F 2

Premises used: CharP.cast_eq_zero, HMul.hMul, WeierstrassCurve.a₃, HPow.hPow, HAdd.hAdd, 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 2
heq : E.j = E'.j
of_j_ne_zero : ∀ (C : VariableChange F) [(C • E).IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
of_j_eq_zero : ∀ (C : VariableChange F) [(C • E).IsCharTwoJEqZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

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

Premises used: Polynomial.C, WeierstrassCurve.exists_variableChange_isCharTwoNF
-- 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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
of_j_ne_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
of_j_ne_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJEqZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

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

Premises used: WeierstrassCurve.exists_variableChange_isCharTwoNF
-- 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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
⊢ (C • E).a₆ = (C' • E').a₆

Tactic:
simp_rw [← variableChange_j E C, ← variableChange_j E' C',
        j_of_isCharTwoJNeZeroNF_of_char_two, one_div, inv_inj] at heq

Premises used: WeierstrassCurve.variableChange_j, inv_inj, one_div, WeierstrassCurve.j_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
of_j_ne_zero : ∀ (C'' : VariableChange F) (hC : C'' • C • E = C' • E'), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_ne_zero _ _ heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_two_of_j_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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'' * C) • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
use C'⁻¹ * C'' * C