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 2
heq : E.j = E'.j
of_j_ne_zero : ∀ (C : VariableChange F) [(C • E).IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_eq_zero : ∀ (C : VariableChange F) [(C • E).IsCharTwoJEqZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharTwoNF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_ne_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharTwoNF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
of_j_ne_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_ne_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJEqZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharTwoNF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have heq₁ : (C • E).a₆ = (C' • E').a₆
Tactic: simp_rw [← variableChange_j E C, ← variableChange_j E' C',
        j_of_isCharTwoJNeZeroNF_of_char_two, one_div, inv_inj] 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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
⊢ ∃ (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_two_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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
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 2
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
heq : (C • E).a₆ = (C' • E').a₆
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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (C • E).j ≠ 0
Tactic: have h := (C • E).j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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_isCharTwoJEqZeroNF_of_char_two] 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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_eq_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharTwoNF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
of_j_eq_zero : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJNeZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'
have of_j_eq_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJEqZeroNF], ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharTwoNF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (C' • E').j ≠ 0
Tactic: have h := (C' • E').j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJNeZeroNF
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_isCharTwoJEqZeroNF_of_char_two] 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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
⊢ ∃ (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_two_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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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 2
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharTwoJEqZeroNF
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
inst_5 : E.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (↑E.Δ' : F) ≠ 0
Tactic: have h := 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.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
h : (↑E.Δ' : F) ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have h₁ : E.a₂ ≠ 0 ∧ E.a₆ ≠ 0
Tactic: rw [E.coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff, neg_ne_zero,
    pow_ne_zero_iff three_ne_zero] at h
Cleared hypotheses: h
-- 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
h : E.a₂ ≠ 0 ∧ E.a₆ ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₂ : E.a₂ ≠ 0
Tactic: obtain ⟨ha₂, ha₆⟩ := h
Cleared hypotheses: h
-- 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
h : E.a₂ ≠ 0 ∧ E.a₆ ≠ 0
ha₂ : E.a₂ ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₆ : E.a₆ ≠ 0
Tactic: obtain ⟨ha₂, ha₆⟩ := h
Cleared hypotheses: h
-- 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
⊢ ∃ (C : VariableChange F), C • E = E'
have h : (↑E'.Δ' : F) ≠ 0
Tactic: have h := 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.IsCharThreeJNeZeroNF
inst_6 : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
h : (↑E'.Δ' : F) ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have h₁ : E'.a₂ ≠ 0 ∧ E'.a₆ ≠ 0
Tactic: rw [E'.coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff, neg_ne_zero,
    pow_ne_zero_iff three_ne_zero] at h
Cleared hypotheses: h
-- 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
h : E'.a₂ ≠ 0 ∧ E'.a₆ ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₂' : E'.a₂ ≠ 0
Tactic: obtain ⟨ha₂', ha₆'⟩ := h
Cleared hypotheses: h
-- 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
h : E'.a₂ ≠ 0 ∧ E'.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
⊢ ∃ (C : VariableChange F), C • E = E'
have ha₆' : E'.a₆ ≠ 0
Tactic: obtain ⟨ha₂', ha₆'⟩ := 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
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
⊢ Ne.{u_1 + 1} (α := F) 2 0
have rw : Ne.{u_1 + 1} (α := F) 1 0
Tactic: rw [show (2 : F) = -1 by linear_combination CharP.cast_eq_zero F 3, neg_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.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
⊢ ∃ (C : VariableChange F), C • E = E'
have this : NeZero.{u_1} (R := F) 2
Tactic: haveI : NeZero (2 : F) := NeZero.mk <| by
    rw [show (2 : F) = -1 by linear_combination CharP.cast_eq_zero F 3, neg_ne_zero]
    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.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
⊢ ∃ (C : VariableChange F), C • E = E'
have obtain : ∀ (u : F) (hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₂ / E'.a₂) 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 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₂
⊢ u ≠ 0
have rw : E.a₂ ≠ 0 ∧ E'.a₂ ≠ 0
Tactic: rw [← pow_ne_zero_iff two_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.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₂
⊢ ∃ (C : VariableChange F), C • E = E'
have hu0 : u ≠ 0
Tactic: have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff two_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.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
⊢ ∃ (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 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 = 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