awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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'
h₅ h₆ : E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'

Tactic:
rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

Premises used: inv_mul_cancel, one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 • E).j ≠ 0

Tactic:
have h := (C • E).j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ Ne.{u_1 + 1} (α := F) 0 0

Tactic:
rw [variableChange_j, heq, ← variableChange_j E' C',
        j_of_isCharTwoJEqZeroNF_of_char_two] at h

Premises used: WeierstrassCurve.variableChange_j, WeierstrassCurve.j_of_isCharTwoJEqZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : Ne.{u_1 + 1} (α := F) 0 0
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : Ne.{u_1 + 1} (α := F) 0 0
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exact False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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'
of_j_eq_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsCharTwoJEqZeroNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharTwoNF

Premises used: WeierstrassCurve.exists_variableChange_isCharTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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' • E').j ≠ 0

Tactic:
have h := (C' • E').j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ Ne.{u_1 + 1} (α := F) 0 0

Tactic:
rw [variableChange_j, ← heq, ← variableChange_j E C,
        j_of_isCharTwoJEqZeroNF_of_char_two] at h

Premises used: WeierstrassCurve.variableChange_j, WeierstrassCurve.j_of_isCharTwoJEqZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : Ne.{u_1 + 1} (α := F) 0 0
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : Ne.{u_1 + 1} (α := F) 0 0
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exact False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
of_j_eq_zero : ∀ (C'' : VariableChange F) (hC : C'' • C • E = C' • E'), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_eq_zero (C • E) (C' • E')

Premises used: HSMul.hSMul, _private.0.WeierstrassCurve.exists_variableChange_of_char_two_of_j_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : VariableChange F), C • E = E'

Tactic:
use C'⁻¹ * C'' * C
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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'
h₅ h₆ : E' = E'
⊢ (C'⁻¹ * C'' * C) • E = E'

Tactic:
rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

Premises used: inv_mul_cancel, one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ (↑E.Δ' : F) ≠ 0

Tactic:
have h := E.Δ'.ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ 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

Premises used: WeierstrassCurve.coe_Δ', neg_ne_zero, three_ne_zero, WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF_of_char_three, pow_ne_zero_iff, mul_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ E.a₂ ≠ 0

Tactic:
obtain ⟨ha₂, ha₆⟩ := h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ E.a₆ ≠ 0

Tactic:
obtain ⟨ha₂, ha₆⟩ := h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ (↑E'.Δ' : F) ≠ 0

Tactic:
have h := E'.Δ'.ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ 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

Premises used: WeierstrassCurve.coe_Δ', neg_ne_zero, three_ne_zero, WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF_of_char_three, pow_ne_zero_iff, mul_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ E'.a₂ ≠ 0

Tactic:
obtain ⟨ha₂', ha₆'⟩ := h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ E'.a₆ ≠ 0

Tactic:
obtain ⟨ha₂', ha₆'⟩ := h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ Eq.{u_1 + 1} (α := F) 2 (-1)

Tactic:
linear_combination CharP.cast_eq_zero F 3

Premises used: CharP.cast_eq_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
rw : Ne.{u_1 + 1} (α := F) 1 0
⊢ Ne.{u_1 + 1} (α := F) 2 0

Tactic:
rw [show (2 : F) = -1 by linear_combination CharP.cast_eq_zero F 3, neg_ne_zero]

Premises used: neg_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
obtain : ∀ (u : F) (hu : HPow.hPow (β := ℕ) u 2 = E.a₂ / E'.a₂), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₂ / E'.a₂) 2

Premises used: HDiv.hDiv, WeierstrassCurve.a₂, IsSepClosed.exists_pow_nat_eq, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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₂
rw : E.a₂ ≠ 0 ∧ E'.a₂ ≠ 0
⊢ u ≠ 0

Tactic:
rw [← pow_ne_zero_iff two_ne_zero, hu, div_ne_zero_iff]

Premises used: div_ne_zero_iff, two_ne_zero, pow_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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₂
⊢ E.a₂ ≠ 0 ∧ E'.a₂ ≠ 0

Tactic:
⟨ha₂, ha₂'⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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₂
⊢ E.a₂ ≠ 0 ∧ E'.a₂ ≠ 0

Tactic:
exact ⟨ha₂, ha₂'⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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

Tactic:
have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff two_ne_zero, hu, div_ne_zero_iff]
    exact ⟨ha₂, ha₂'⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, 0, 0, 0⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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₄
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'

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) * (0 + HMul.hMul (α := F) 2 0) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₁ = E'.a₁

Tactic:
simp_rw [variableChange_a₁, a₁_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.a₁_of_isCharThreeJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) * (0 + HMul.hMul (α := F) 2 0) = 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : (E.a₂ - HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 3 0 - HPow.hPow (α := F) (β := ℕ) 0 2) / (E.a₂ / E'.a₂) = E'.a₂
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } 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]

Premises used: Units.val_inv_eq_inv_val, inv_mul_eq_div, WeierstrassCurve.variableChange_a₂, inv_pow, Units.val_mk0, WeierstrassCurve.a₁_of_isCharThreeJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ (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 [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 : HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 3 * (0 + HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 2 0) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, a₁_of_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.a₃_of_isCharThreeJNeZeroNF, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.a₁_of_isCharThreeJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ HPow.hPow (β := ℕ) (↑((Units.mk0 u hu0)⁻¹ : Fˣ) : F) 3 * (0 + HMul.hMul (α := F) 0 0 + HMul.hMul (α := F) 2 0) = 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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 :
  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
⊢ (HSMul.hSMul (α := VariableChange F) { u := Units.mk0 u hu0, r := 0, s := 0, t := 0 : VariableChange F } E).a₄ = E'.a₄

Tactic:
simp_rw [variableChange_a₄, a₁_of_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF,
      a₄_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.a₃_of_isCharThreeJNeZeroNF, WeierstrassCurve.a₄_of_isCharThreeJNeZeroNF, WeierstrassCurve.variableChange_a₄, WeierstrassCurve.a₁_of_isCharThreeJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
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
⊢ 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:
ring1