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
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
have h : (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) * (0 + HMul.hMul (α := F) 2 0) = 0
Tactic: simp_rw [variableChange_a₁, a₁_of_isCharThreeJNeZeroNF]
-- 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 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ (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) 3 0 - HPow.hPow (α := F) (β := ℕ) 0 2) / (E.a₂ / E'.a₂) = E'.a₂
Tactic: simp_rw [variableChange_a₂, a₁_of_isCharThreeJNeZeroNF, Units.val_inv_eq_inv_val,
      Units.val_mk0, inv_pow, inv_mul_eq_div, hu]
-- 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 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
have h : HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 3 * (0 + HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 2 0) = 0
Tactic: simp_rw [variableChange_a₃, a₁_of_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF]
-- 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 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄
have h : HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 4 *
    (0 - HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 2 0 * E.a₂ - (0 + HMul.hMul (α := F) 0 0) * 0 +
        3 * HPow.hPow (α := F) (β := ℕ) 0 2 -
      HMul.hMul (α := F) 2 0 * 0) =
  0
Tactic: simp_rw [variableChange_a₄, a₁_of_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF,
      a₄_of_isCharThreeJNeZeroNF]
-- 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 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₆ = E'.a₆
have heq₁ : -HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆ = -HPow.hPow (β := ℕ) E'.a₂ 3 * E.a₆
Tactic: simp_rw [j_of_isCharThreeJNeZeroNF_of_char_three, div_eq_div_iff ha₆ ha₆'] at heq
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
heq : -HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆ = -HPow.hPow (β := ℕ) E'.a₂ 3 * E.a₆
⊢ (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 + HPow.hPow (α := F) (β := ℕ) 0 2 * E.a₂ + HPow.hPow (α := F) (β := ℕ) 0 3 -
          HMul.hMul (α := F) 0 0 -
        HPow.hPow (α := F) (β := ℕ) 0 2 -
      HMul.hMul (α := F) 0 0 * 0) /
    HPow.hPow (β := ℕ) (E.a₂ / E'.a₂) 3 =
  E'.a₆
Tactic: simp_rw [variableChange_a₆, a₁_of_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF,
      a₄_of_isCharThreeJNeZeroNF, Units.val_inv_eq_inv_val, Units.val_mk0,
      inv_pow, inv_mul_eq_div, pow_mul u 2 3, hu]
-- 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 3
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero.{u_1} (R := F) 2
u : F
hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
heq : -HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆ = -HPow.hPow (β := ℕ) E'.a₂ 3 * E.a₆
⊢ (E.a₆ + HMul.hMul (α := F) 0 0 + HPow.hPow (α := F) (β := ℕ) 0 2 * E.a₂ + HPow.hPow (α := F) (β := ℕ) 0 3 -
            HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 0 0 * 0) /
      HPow.hPow (β := ℕ) (E.a₂ / E'.a₂) 3 =
    E'.a₆
have h : E.a₆ * HPow.hPow (β := ℕ) E'.a₂ 3 = HPow.hPow (β := ℕ) E.a₂ 3 * E'.a₆
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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
⊢ ∃ (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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : (↑E.Δ' : F) ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₅ : E.a₄ ≠ 0
Tactic: rw [E.coe_Δ', Δ_of_isShortNF_of_char_three, neg_ne_zero, pow_ne_zero_iff three_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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : (↑E'.Δ' : F) ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₄'₁ : E'.a₄ ≠ 0
Tactic: rw [E'.coe_Δ', Δ_of_isShortNF_of_char_three, neg_ne_zero, pow_ne_zero_iff three_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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 4 0
have rw : Ne.{u_1 + 1} (α := F) 1 0
Tactic: rw [show (4 : F) = 1 by linear_combination CharP.cast_eq_zero F 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
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have this : NeZero.{u_1} (R := F) 4
Tactic: haveI : NeZero (4 : F) := NeZero.mk <| by
    rw [show (4 : F) = 1 by linear_combination CharP.cast_eq_zero F 3]
    exact one_ne_zero
-- 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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
⊢ ∃ (C : VariableChange F), C • E = E'
have obtain : ∀ (u : F) (hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₄ / E'.a₄) 4
-- 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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
⊢ ∃ (C : VariableChange F), C • E = E'
have obtain : ∀ (r : F) (hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0),
  ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨r, hr⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 3 3
    1 _ (E.a₆ - u ^ 6 * E'.a₆) (by simp) (by simp) ha₄
-- 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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
⊢ u ≠ 0
have rw : E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0
Tactic: rw [← pow_ne_zero_iff four_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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
⊢ ∃ (C : VariableChange F), C • E = E'
have hu0 : u ≠ 0
Tactic: have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff four_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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have h : HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E = E'
Tactic: use ⟨Units.mk0 u hu0, r, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E = E'
have h : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E = E'
have h₁ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E = E'
have h₂ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E = E'
have h₃ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
h :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
h₃ :
  (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄
⊢ HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E = E'
have h₄ : (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁
have h : (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) * (0 + HMul.hMul (α := F) 2 0) = 0
Tactic: simp_rw [variableChange_a₁, a₁_of_isShortNF]
-- 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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₂ = E'.a₂
have h : HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 2 *
    (0 - HMul.hMul (α := F) 0 0 + 0 * r - HPow.hPow (α := F) (β := ℕ) 0 2) =
  0
Tactic: simp_rw [variableChange_a₂, a₁_of_isShortNF, a₂_of_isShortNF,
      show (3 : F) = 0 from CharP.cast_eq_zero F 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 3
inst_5 : E.IsShortNF
inst_6 : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero.{u_1} (R := F) 4
u : F
hu : HPow.hPow (β := ℕ) u 4 = E.a₄ / E'.a₄
r : F
hr : 1 * HPow.hPow (β := ℕ) r 3 + E.a₄ * r + (E.a₆ - HPow.hPow (β := ℕ) u 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := r, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃
have h : HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 3 * (0 + r * 0 + HMul.hMul (α := F) 2 0) = 0
Tactic: simp_rw [variableChange_a₃, a₁_of_isShortNF, a₃_of_isShortNF]