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.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 : (E.a₄ - HMul.hMul (α := F) 0 0 + 2 * r * 0 - (0 + r * 0) * 0 + 0 * HPow.hPow (β := ℕ) r 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, hu,
      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 : (E.a₆ + r * E.a₄ + HPow.hPow (β := ℕ) r 2 * 0 + HPow.hPow (β := ℕ) r 3 - HMul.hMul (α := F) 0 0 -
        HPow.hPow (α := F) (β := ℕ) 0 2 -
      r * 0 * 0) /
    HPow.hPow (β := ℕ) u 6 =
  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]
-- 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
⊢ (E.a₆ + r * E.a₄ + HPow.hPow (β := ℕ) r 2 * 0 + HPow.hPow (β := ℕ) r 3 - HMul.hMul (α := F) 0 0 -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        r * 0 * 0) /
      HPow.hPow (β := ℕ) u 6 =
    E'.a₆
have h : E.a₆ + r * E.a₄ + HPow.hPow (β := ℕ) r 3 = HPow.hPow (β := ℕ) u 6 * E'.a₆
Tactic: simp [field]
-- 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
heq : E.j = E'.j
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_ne_zero : ∀ (C : VariableChange F) [(C • E).IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharThreeNF
-- 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
heq : E.j = E'.j
of_j_ne_zero : ∀ (C : VariableChange F) [(C • E).IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_eq_zero : ∀ (C : VariableChange F) [(C • E).IsShortNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharThreeNF
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_ne_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
of_j_ne_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_ne_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsShortNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharThreeJNeZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_ne_zero : ∀ [(C • E).IsCharThreeJNeZeroNF] (C' : VariableChange F) (heq : (C • E).j = (C' • E').j)
  [(C' • E').IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: rw [← variableChange_j E C, ← variableChange_j E' C'] at heq
Cleared hypotheses: heq, inst_5, C', inst_6
-- 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
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_ne_zero : ∀ (C'' : VariableChange F) (hC : C'' • C • E = C' • E'), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_ne_zero _ _ 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
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (C'⁻¹ * C'' * C) • E = E'
Tactic: use C'⁻¹ * C'' * C
-- 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
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h : (C'⁻¹ * C'') • C • E = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₁ : C'⁻¹ • C'' • C • E = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₂ : C'⁻¹ • C' • E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
h₂ : C'⁻¹ • C' • E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₃ : (C'⁻¹ * C') • E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
h₂ : C'⁻¹ • C' • E' = E'
h₃ : (C'⁻¹ * C') • E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₄ : HSMul.hSMul (α := VariableChange F) 1 E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
h₂ : C'⁻¹ • C' • E' = E'
h₃ : (C'⁻¹ * C') • E' = E'
h₄ : HSMul.hSMul (α := VariableChange F) 1 E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₅ : E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (C • E).j ≠ 0
Tactic: have h := (C • E).j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
h : (C • E).j ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have h₁ : Ne.{u_1 + 1} (α := F) 0 0
Tactic: rw [variableChange_j, heq, ← variableChange_j E' C', j_of_isShortNF_of_char_three] at h
Cleared hypotheses: h
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_eq_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
of_j_eq_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharThreeJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_eq_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsShortNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsCharThreeJNeZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (C' • E').j ≠ 0
Tactic: have h := (C' • E').j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsCharThreeJNeZeroNF
h : (C' • E').j ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have h₁ : Ne.{u_1 + 1} (α := F) 0 0
Tactic: rw [variableChange_j, ← heq, ← variableChange_j E C, j_of_isShortNF_of_char_three] at h
Cleared hypotheses: h
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_eq_zero : ∀ (C'' : VariableChange F) (hC : C'' • C • E = C' • E'), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_eq_zero (C • E) (C' • E')
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (C'⁻¹ * C'' * C) • E = E'
Tactic: use C'⁻¹ * C'' * C
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h : (C'⁻¹ * C'') • C • E = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₁ : C'⁻¹ • C'' • C • E = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₂ : C'⁻¹ • C' • E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
h₂ : C'⁻¹ • C' • E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₃ : (C'⁻¹ * C') • E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
h₂ : C'⁻¹ • C' • E' = E'
h₃ : (C'⁻¹ * C') • E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₄ : HSMul.hSMul (α := VariableChange F) 1 E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
h : (C'⁻¹ * C'') • C • E = E'
h₁ : C'⁻¹ • C'' • C • E = E'
h₂ : C'⁻¹ • C' • E' = E'
h₃ : (C'⁻¹ * C') • E' = E'
h₄ : HSMul.hSMul (α := VariableChange F) 1 E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'
have h₅ : E' = E'
Tactic: rw [mul_smul, 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 E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : p ≠ 2
hchar3 : p ≠ 3
heq : E.j = E'.j
⊢ ∃ (C : VariableChange F), C • E = E'
have hchar2₁ : Ne.{u_1 + 1} (α := F) 2 0
Tactic: replace hchar2 : (2 : F) ≠ 0 := CharP.cast_ne_zero_of_ne_of_prime F Nat.prime_two hchar2
Cleared hypotheses: hchar2
-- 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
hchar3 : p ≠ 3
heq : E.j = E'.j
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
⊢ ∃ (C : VariableChange F), C • E = E'
have hchar3₁ : Ne.{u_1 + 1} (α := F) 3 0
Tactic: replace hchar3 : (3 : F) ≠ 0 := CharP.cast_ne_zero_of_ne_of_prime F Nat.prime_three hchar3
Cleared hypotheses: 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
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
⊢ ∃ (C : VariableChange F), C • E = E'
have this : NeZero.{u_1} (R := F) 2
Tactic: haveI := NeZero.mk hchar2
-- 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 : NeZero.{u_1} (R := F) 2
⊢ Ne.{u_1 + 1} (α := F) 4 0
have this₁ : HPow.hPow (α := F) (β := ℕ) 2 2 ≠ 0
Tactic: have := pow_ne_zero 2 hchar2
-- 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 : NeZero.{u_1} (R := F) 2
⊢ ∃ (C : VariableChange F), C • E = E'
have this₁ : NeZero.{u_1} (R := F) 4
Tactic: haveI : NeZero (4 : F) := NeZero.mk <| by
    have := pow_ne_zero 2 hchar2
    norm_num1 at this
    exact this
-- 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 : NeZero.{u_1} (R := F) 4
⊢ Ne.{u_1 + 1} (α := F) 6 0
have this₁ : HMul.hMul (α := F) 2 3 ≠ 0
Tactic: have := mul_ne_zero 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
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 : NeZero.{u_1} (R := F) 4
⊢ ∃ (C : VariableChange F), C • E = E'
have this₁ : NeZero.{u_1} (R := F) 6
Tactic: haveI : NeZero (6 : F) := NeZero.mk <| by
    have := mul_ne_zero hchar2 hchar3
    norm_num1 at this
    exact this
-- 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 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
⊢ ∃ (C : VariableChange F), C • E = E'
have inr : ∀
  (this :
    ∀ (E : WeierstrassCurve F) [inst_5 : 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 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 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
inr :
  ∀
    (this :
      ∀ (E : WeierstrassCurve F) [inst_5 : 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_5 : E.IsElliptic] (heq : E.j = E'.j),
  E.IsShortNF → ∃ (C : VariableChange F), C • E = E'
Tactic: wlog _ : E.IsShortNF generalizing E
Cleared hypotheses: heq