awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
⊢ ∃ (C : VariableChange F), C • E = E'
have hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
Tactic: have hu4 : u ^ 4 = E.a₄ / E'.a₄ := by
    rw [pow_mul u 2 2, hu]
    simp [field]
    linear_combination -heq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
⊢ HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
have rw : HPow.hPow (β := ℕ) (E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)) 3 = E.a₆ / E'.a₆
Tactic: rw [pow_mul u 2 3, hu]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
⊢ HPow.hPow (β := ℕ) (E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)) 3 = E.a₆ / E'.a₆
have simp : HPow.hPow (β := ℕ) E.a₆ 2 * HPow.hPow (β := ℕ) E'.a₄ 3 = HPow.hPow (β := ℕ) E'.a₆ 2 * HPow.hPow (β := ℕ) E.a₄ 3
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
⊢ ∃ (C : VariableChange F), C • E = E'
have hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
Tactic: have hu6 : u ^ 6 = E.a₆ / E'.a₆ := by
    rw [pow_mul u 2 3, hu]
    simp [field]
    linear_combination -heq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
⊢ u ≠ 0
have rw : E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0
Tactic: rw [← pow_ne_zero_iff four_ne_zero, hu4, 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_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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
⊢ ∃ (C : VariableChange F), C • E = E'
have hu0 : u ≠ 0
Tactic: have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff four_ne_zero, hu4, 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_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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have h : HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'
Tactic: use ⟨Units.mk0 u hu0, 0, 0, 0⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'
have h : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, 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_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'
have h₁ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, 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_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'
have h₂ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, 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_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'
have h₃ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, 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_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h_1 : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_2 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
h₃ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E = E'
have h₄ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, 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_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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄
have h : (E.a₄ - HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 2 0 * 0 - (0 + HMul.hMul (α := F) 0 0) * 0 +
        3 * HPow.hPow (α := F) (β := ℕ) 0 2 -
      HMul.hMul (α := F) 2 0 * 0) /
    (E.a₄ / E'.a₄) =
  E'.a₄
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, hu4]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
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
ha₆' : E'.a₆ ≠ 0
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
hu6 : HPow.hPow (β := ℕ) u 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₆ = E'.a₆
have h : (E.a₆ + 0 * E.a₄ + HPow.hPow (α := F) (β := ℕ) 0 2 * 0 + HPow.hPow (α := F) (β := ℕ) 0 3 - HMul.hMul (α := F) 0 0 -
        HPow.hPow (α := F) (β := ℕ) 0 2 -
      HMul.hMul (α := F) 0 0 * 0) /
    (E.a₆ / 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, hu6]
-- 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
heq : E.j = E'.j
⊢ ∃ (C : VariableChange F), C • E = E'
have obtain : ∀ (p : ℕ), CharP F p → ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨p, _⟩ := CharP.exists F
-- 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
heq : E.j = E'.j
p : ℕ
h : CharP F p
⊢ ∃ (C : VariableChange F), C • E = E'
have pos : ∀ (hchar2 : p = 2), ∃ (C : VariableChange F), C • E = E'
Tactic: by_cases hchar2 : p = 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
heq : E.j = E'.j
p : ℕ
h : CharP F p
pos : ∀ (hchar2 : p = 2), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have neg : ∀ (hchar2 : ¬p = 2), ∃ (C : VariableChange F), C • E = E'
Tactic: by_cases hchar2 : p = 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
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : p = 2
⊢ ∃ (C : VariableChange F), C • E = E'
have h : CharP F 2
Tactic: subst hchar2
Cleared hypotheses: p, h, hchar2
-- 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
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : ¬p = 2
⊢ ∃ (C : VariableChange F), C • E = E'
have pos : ∀ (hchar3 : p = 3), ∃ (C : VariableChange F), C • E = E'
Tactic: by_cases hchar3 : p = 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
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : ¬p = 2
pos : ∀ (hchar3 : p = 3), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have neg : ∀ (hchar3 : ¬p = 3), ∃ (C : VariableChange F), C • E = E'
Tactic: by_cases hchar3 : p = 3
-- 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
heq : E.j = E'.j
p : ℕ
h : CharP F p
hchar2 : ¬p = 2
hchar3 : p = 3
⊢ ∃ (C : VariableChange F), C • E = E'
have h : CharP F 3
Tactic: subst hchar3
Cleared hypotheses: p, h, hchar2, hchar3
-- 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
heq : E.j = E'.j
p : ℕ
h_1 : CharP F p
hchar2 : ¬p = 2
hchar3 : p = 3
h : CharP F 3
⊢ ∃ (C : VariableChange F), C • E = E'
have hchar2₁ : ¬Eq (α := ℕ) 3 2
Tactic: subst hchar3
Cleared hypotheses: p, h_1, hchar2, hchar3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] = P
have h : ∀ (n : Fin (Nat.succ 0).succ.succ), ![P x, P y, P z] n = P n
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n
have h : ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
h :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![P x, P y, P z] n = P n
have h₁ : ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
h :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![P x, P y, P z] n = P n
have h₂ : ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f : (a : R) → S) ∘ (u • P) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)
have h : ∀ (n : Fin 3),
  ((⇑f : (a : R) → S) ∘ (u • P)) n =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) n
Tactic: ext n