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 : E.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
heq : E.j = E'.j
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have inr : ∀ (C : VariableChange F) (hE : (C • E).IsShortNF), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C, hE⟩ := E.exists_variableChange_isShortNF
-- 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
p : ℕ
inst_4 : CharP F p
heq : E.j = E'.j
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
C : VariableChange F
hE : (C • E).IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have heq₁ : (C • E).j = E'.j
Tactic: rw [← variableChange_j E C] at heq
Cleared hypotheses: heq, hE
-- 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
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
C : VariableChange F
heq : (C • E).j = E'.j
hE : (C • E).IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have inr : ∀ (C' : VariableChange F) (hC : C' • C • E = E'), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', hC⟩ := this _ heq hE
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have inr : ∀
  (this :
    ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
      ∃ (C : VariableChange F), C • E = E'),
  ¬E'.IsShortNF → ∃ (C : VariableChange F), C • E = E'
Tactic: wlog _ : E'.IsShortNF generalizing E'
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
inr :
  ∀
    (this :
      ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
        ∃ (C : VariableChange F), C • E = E'),
    ¬E'.IsShortNF → ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have wlog : ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j),
  E'.IsShortNF → ∃ (C : VariableChange F), C • E = E'
Tactic: wlog _ : E'.IsShortNF generalizing E'
Cleared hypotheses: 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have inr : ∀ (C : VariableChange F) (hE' : (C • E').IsShortNF), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C, hE'⟩ := E'.exists_variableChange_isShortNF
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
hE' : (C • E').IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have heq₁ : E.j = (C • E').j
Tactic: rw [← variableChange_j E' C] at heq
Cleared hypotheses: heq, hE'
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have inr : ∀ (C' : VariableChange F) (hC : C' • E = C • E'), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', hC⟩ := this _ heq hE'
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
⊢ (C⁻¹ * C') • E = E'
have rw : C⁻¹ • C' • E = E'
Tactic: rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
rw : C⁻¹ • C' • E = E'
⊢ (C⁻¹ * C') • E = E'
have rw₁ : C⁻¹ • C • E' = E'
Tactic: rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
rw : C⁻¹ • C' • E = E'
rw₁ : C⁻¹ • C • E' = E'
⊢ (C⁻¹ * C') • E = E'
have rw₂ : (C⁻¹ * C) • E' = E'
Tactic: rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
rw : C⁻¹ • C' • E = E'
rw₁ : C⁻¹ • C • E' = E'
rw₂ : (C⁻¹ * C) • E' = E'
⊢ (C⁻¹ * C') • E = E'
have rw₃ : HSMul.hSMul (α := VariableChange F) 1 E' = E'
Tactic: rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
-- 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' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
rw : C⁻¹ • C' • E = E'
rw₁ : C⁻¹ • C • E' = E'
rw₂ : (C⁻¹ * C) • E' = E'
rw₃ : HSMul.hSMul (α := VariableChange F) 1 E' = E'
⊢ (C⁻¹ * C') • E = E'
have rw₄ : E' = E'
Tactic: rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
-- 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
heq : E.j = E'.j
h_1 : E'.IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have heq₁ : HPow.hPow (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
  HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
Tactic: simp_rw [j, Units.val_inv_eq_inv_val, inv_mul_eq_div,
    div_eq_div_iff E.Δ'.ne_zero E'.Δ'.ne_zero, coe_Δ', Δ_of_isShortNF, c₄_of_isShortNF] at heq
Cleared hypotheses: heq
-- 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
⊢ Ne.{u_1 + 1} (α := F) 47775744 0
have this₁ : HPow.hPow (α := F) (β := ℕ) 2 16 * HPow.hPow (α := F) (β := ℕ) 3 6 ≠ 0
Tactic: have := mul_ne_zero (pow_ne_zero 16 hchar2) (pow_ne_zero 6 hchar3)
-- 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_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq :
  HPow.hPow (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
this : Invertible (α := F) 47775744 := invertibleOfNonzero ⋯
⊢ HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
have rw : 47775744 * (HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2) =
  47775744 * (HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2)
Tactic: rw [← mul_right_inj_of_invertible (47775744 : F)]
-- 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 (β := ℕ) (-48 * E.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E'.a₄ 3 + 27 * HPow.hPow (β := ℕ) E'.a₆ 2)) =
    HPow.hPow (β := ℕ) (-48 * E'.a₄) 3 * (-16 * (4 * HPow.hPow (β := ℕ) E.a₄ 3 + 27 * HPow.hPow (β := ℕ) E.a₆ 2))
⊢ ∃ (C : VariableChange F), C • E = E'
have heq₁ : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
Tactic: replace heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2 := by
    letI : Invertible (47775744 : F) := invertibleOfNonzero <| by
      have := mul_ne_zero (pow_ne_zero 16 hchar2) (pow_ne_zero 6 hchar3)
      norm_num1 at this
      exact this
    rw [← mul_right_inj_of_invertible (47775744 : F)]
    linear_combination heq
Cleared hypotheses: 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
⊢ ∃ (C : VariableChange F), C • E = E'
have pos : ∀ (ha₄ : E.a₄ = 0), ∃ (C : VariableChange F), C • E = E'
Tactic: by_cases ha₄ : E.a₄ = 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
pos : ∀ (ha₄ : E.a₄ = 0), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have neg : ∀ (ha₄ : ¬E.a₄ = 0), ∃ (C : VariableChange F), C • E = E'
Tactic: by_cases ha₄ : E.a₄ = 0
-- 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
⊢ ∃ (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_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : E.a₄ = 0
ha₆ : (↑E.Δ' : F) ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₇ : HMul.hMul (α := F) (-16) 27 ≠ 0 ∧ E.a₆ ≠ 0
Tactic: rw [coe_Δ', Δ_of_isShortNF, ha₄, zero_pow three_ne_zero, mul_zero, zero_add, ← mul_assoc,
      mul_ne_zero_iff, pow_ne_zero_iff two_ne_zero] at ha₆
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_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : E.a₄ = 0
ha₆ : HMul.hMul (α := F) (-16) 27 ≠ 0 ∧ E.a₆ ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₇ : E.a₆ ≠ 0
Tactic: replace ha₆ := ha₆.2
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_1 E'_1 : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'_1.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
h : E.IsShortNF
E' : WeierstrassCurve F
inst_6 : E'.IsElliptic
h_1 : E'.IsShortNF
heq : HPow.hPow (β := ℕ) E.a₄ 3 * HPow.hPow (β := ℕ) E'.a₆ 2 = HPow.hPow (β := ℕ) E'.a₄ 3 * HPow.hPow (β := ℕ) E.a₆ 2
ha₄ : E.a₄ = 0
ha₆ : E.a₆ ≠ 0
⊢ E'.a₄ = 0
have heq₁ : HPow.hPow (β := ℕ) E'.a₄ 3 = 0 ∨ HPow.hPow (β := ℕ) E.a₆ 2 = 0
Tactic: rw [ha₄, zero_pow three_ne_zero, zero_mul, zero_eq_mul] at heq
Cleared hypotheses: heq, ha₄, ha₆