awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₃ = E'.a₃
h₃ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₄ = E'.a₄
⊢ HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'
have h₄ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₆ = E'.a₆
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁
have h : 1 * (1 + 2 * s) = 1
Tactic: simp_rw [variableChange_a₁, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₂ = E'.a₂
have h : HPow.hPow (α := F) (β := ℕ) 1 2 * (E.a₂ - s * 1 + HMul.hMul (α := F) 3 0 - HPow.hPow (β := ℕ) s 2) = E'.a₂
Tactic: simp_rw [variableChange_a₂, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₃ = E'.a₃
have h : HPow.hPow (α := F) (β := ℕ) 1 3 * (0 + 0 * E.a₁ + HMul.hMul (α := F) 2 0) = 0
Tactic: simp_rw [variableChange_a₃, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₄ = E'.a₄
have h : HPow.hPow (α := F) (β := ℕ) 1 4 *
    (0 - s * 0 + HMul.hMul (α := F) 2 0 * E.a₂ - (0 + 0 * s) * E.a₁ + 3 * HPow.hPow (α := F) (β := ℕ) 0 2 - 2 * s * 0) =
  0
Tactic: simp_rw [variableChange_a₄, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF,
      a₄_of_isCharTwoJNeZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₆ = E'.a₆
have h : HPow.hPow (α := F) (β := ℕ) 1 6 *
    (E'.a₆ + 0 * E.a₄ + HPow.hPow (α := F) (β := ℕ) 0 2 * E.a₂ + HPow.hPow (α := F) (β := ℕ) 0 3 - 0 * E.a₃ -
        HPow.hPow (α := F) (β := ℕ) 0 2 -
      HMul.hMul (α := F) 0 0 * E.a₁) =
  E'.a₆
Tactic: simp_rw [variableChange_a₆, inv_one, Units.val_one, heq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₃ : (↑E.Δ' : F) ≠ 0
Tactic: have ha₃ := E.Δ'.ne_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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.Δ' : F) ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₄ : E.a₃ ≠ 0
Tactic: rw [E.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃
Cleared hypotheses: ha₃
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₃' : (↑E'.Δ' : F) ≠ 0
Tactic: have ha₃' := E'.Δ'.ne_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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'.Δ' : F) ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₃'₁ : E'.a₃ ≠ 0
Tactic: rw [E'.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃'
Cleared hypotheses: ha₃'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ Ne.{u_1 + 1} (α := F) 3 0
have rw : Ne.{u_1 + 1} (α := F) 1 0
Tactic: rw [show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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
⊢ ∃ (C : VariableChange F), C • E = E'
have this : NeZero.{u_1} (R := F) 3
Tactic: haveI : NeZero (3 : F) := NeZero.mk <| by
    rw [show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]
    exact one_ne_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ ∃ (C : VariableChange F), C • E = E'
have obtain : ∀ (u : F) (hu : HPow.hPow (β := ℕ) u 3 = E.a₃ / E'.a₃), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₃ / E'.a₃) 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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₃
⊢ ∃ (C : VariableChange F), C • E = E'
have 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'
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₃
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ ∃ (C : VariableChange F), C • E = E'
have 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'
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₃
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
have rw : E.a₃ ≠ 0 ∧ E'.a₃ ≠ 0
Tactic: rw [← pow_ne_zero_iff three_ne_zero, hu, div_ne_zero_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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
⊢ ∃ (C : VariableChange F), C • E = E'
have hu0 : u ≠ 0
Tactic: have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff three_ne_zero, hu, div_ne_zero_iff]
    exact ⟨ha₃, ha₃'⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ ∃ (C : VariableChange F), C • E = E'
have h : HSMul.hSMul (α := VariableChange F)
    { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E =
  E'
Tactic: use ⟨Units.mk0 u hu0, s ^ 2, s, t⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ HSMul.hSMul (α := VariableChange F)
      { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E =
    E'
have 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₁
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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₁
⊢ HSMul.hSMul (α := VariableChange F)
      { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E =
    E'
have 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₂
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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₂
⊢ HSMul.hSMul (α := VariableChange F)
      { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E =
    E'
have 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₃
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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₃
⊢ HSMul.hSMul (α := VariableChange F)
      { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E =
    E'
have 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₄
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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₄
⊢ HSMul.hSMul (α := VariableChange F)
      { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E =
    E'
have 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₆
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₁ =
    E'.a₁
have h : (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) * (0 + 0 * s) = 0
Tactic: simp_rw [variableChange_a₁, a₁_of_isCharTwoJEqZeroNF,
      show (2 : F) = 0 from CharP.cast_eq_zero F 2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₂ =
    E'.a₂
have h : HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 2 *
    (0 - s * 0 + 1 * HPow.hPow (β := ℕ) s 2 - HPow.hPow (β := ℕ) s 2) =
  0
Tactic: simp_rw [variableChange_a₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF,
      show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₃ =
    E'.a₃
have h : (E.a₃ + HPow.hPow (β := ℕ) s 2 * 0 + 0 * t) / (E.a₃ / 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₄ =
    E'.a₄
have h : E.a₄ - s * E.a₃ + HPow.hPow (β := ℕ) s 4 * 3 - s * 2 * t = HPow.hPow (β := ℕ) u 4 * E'.a₄
Tactic: simp [field, variableChange_a₄, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
⊢ (HSMul.hSMul (α := VariableChange F)
        { u := Units.mk0 u hu0, r := HPow.hPow (β := ℕ) s 2, s := s, t := t : VariableChange F } E).a₆ =
    E'.a₆
have 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₆
Tactic: simp [field, variableChange_a₆, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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), C • E = E'
have of_j_ne_zero : ∀ (C : VariableChange F) [(C • E).IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharTwoNF