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 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsCharThreeJNeZeroNF
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'
⊢ ∃ (C : VariableChange F), C • E = E'

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

Premises used: WeierstrassCurve.variableChange_j
-- 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
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst_6 : (C' • E').IsCharThreeJNeZeroNF
of_j_ne_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_three_of_j_ne_zero _ _ heq

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_three_of_j_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
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 : 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 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'
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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
⊢ (C • E).j ≠ 0

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

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

Premises used: WeierstrassCurve.variableChange_j, WeierstrassCurve.j_of_isShortNF_of_char_three
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
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 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
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 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'
of_j_eq_zero₁ : ∀ (C' : VariableChange F) [(C' • E').IsShortNF], ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

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

Premises used: WeierstrassCurve.exists_variableChange_isCharThreeNF
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsCharThreeJNeZeroNF
⊢ (C' • E').j ≠ 0

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

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

Premises used: WeierstrassCurve.variableChange_j, WeierstrassCurve.j_of_isShortNF_of_char_three
-- 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
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsCharThreeJNeZeroNF
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 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsCharThreeJNeZeroNF
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 3
heq : E.j = E'.j
C : VariableChange F
inst_5 : (C • E).IsShortNF
C' : VariableChange F
inst_6 : (C' • E').IsShortNF
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_three_of_j_eq_zero (C • E) (C' • E')

Premises used: _private.0.WeierstrassCurve.exists_variableChange_of_char_three_of_j_eq_zero, HSMul.hSMul
-- 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
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 : 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 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'
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
p : ℕ
inst_4 : CharP F p
hchar2 : p ≠ 2
hchar3 : p ≠ 3
heq : E.j = E'.j
⊢ 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
-- 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
p : ℕ
inst_4 : CharP F p
hchar3 : p ≠ 3
heq : E.j = E'.j
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
⊢ 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
-- 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
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
⊢ NeZero.{u_1} (R := F) 2

Tactic:
haveI := NeZero.mk hchar2
-- 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
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
⊢ HPow.hPow (α := F) (β := ℕ) 2 2 ≠ 0

Tactic:
have := pow_ne_zero 2 hchar2
-- 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
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 : HPow.hPow (α := F) (β := ℕ) 2 2 ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 4 0

Tactic:
norm_num1 at this
-- 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
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 : Ne.{u_1 + 1} (α := F) 4 0
⊢ Ne.{u_1 + 1} (α := F) 4 0

Tactic:
this
-- 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
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 : Ne.{u_1 + 1} (α := F) 4 0
⊢ Ne.{u_1 + 1} (α := F) 4 0

Tactic:
exact this
-- 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
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
⊢ 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
-- 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
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
⊢ HMul.hMul (α := F) 2 3 ≠ 0

Tactic:
have := mul_ne_zero hchar2 hchar3
-- 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
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 : HMul.hMul (α := F) 2 3 ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 6 0

Tactic:
norm_num1 at this
-- 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
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 : Ne.{u_1 + 1} (α := F) 6 0
⊢ Ne.{u_1 + 1} (α := F) 6 0

Tactic:
this
-- 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
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 : Ne.{u_1 + 1} (α := F) 6 0
⊢ Ne.{u_1 + 1} (α := F) 6 0

Tactic:
exact this
-- 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
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
⊢ 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
-- 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
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'
wlog :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j),
    E.IsShortNF → ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
wlog _ : E.IsShortNF generalizing E

Premises used: WeierstrassCurve.IsShortNF
-- 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
p : ℕ
inst_4 : CharP F p
heq : E.j = E'.j
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
inr : ∀ (C : VariableChange F) (hE : (C • E).IsShortNF), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C, hE⟩ := E.exists_variableChange_isShortNF

Premises used: Polynomial.C, WeierstrassCurve.exists_variableChange_isShortNF
-- 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
p : ℕ
inst_4 : CharP F p
heq : E.j = E'.j
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
C : VariableChange F
hE : (C • E).IsShortNF
⊢ (C • E).j = E'.j

Tactic:
rw [← variableChange_j E C] at heq

Premises used: WeierstrassCurve.variableChange_j
-- 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
p : ℕ
inst_4 : CharP F p
heq : E.j = E'.j
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
C : VariableChange F
hE : (C • E).IsShortNF
heq₁ : (C • E).j = E'.j
⊢ (C • E).IsShortNF

Tactic:
rw [← variableChange_j E C] at heq

Premises used: WeierstrassCurve.variableChange_j
-- 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
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
C : VariableChange F
heq : (C • E).j = E'.j
hE : (C • E).IsShortNF
inr : ∀ (C' : VariableChange F) (hC : C' • C • E = E'), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C', hC⟩ := this _ heq hE
-- 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
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
C : VariableChange F
heq : (C • E).j = E'.j
hE : (C • E).IsShortNF
C' : VariableChange F
hC : C' • C • E = E'
rwa rwa₁ rwa₂ rwa₃ : C' • C • E = E'
⊢ (C' * C) • E = E'

Tactic:
rwa [mul_smul]

Premises used: 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
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
this :
  ∀ (E : WeierstrassCurve F) [inst_5 : E.IsElliptic] (heq : E.j = E'.j) (h : E.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h : ¬E.IsShortNF
C : VariableChange F
heq : (C • E).j = E'.j
hE : (C • E).IsShortNF
C' : VariableChange F
hC : C' • C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
exact ⟨C' * C, by rwa [mul_smul]⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
inr :
  ∀
    (this :
      ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
        ∃ (C : VariableChange F), C • E = E'),
    ¬E'.IsShortNF → ∃ (C : VariableChange F), C • E = E'
wlog :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j),
    E'.IsShortNF → ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
wlog _ : E'.IsShortNF generalizing E'

Premises used: WeierstrassCurve.IsShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
inr : ∀ (C : VariableChange F) (hE' : (C • E').IsShortNF), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨C, hE'⟩ := E'.exists_variableChange_isShortNF

Premises used: Polynomial.C, WeierstrassCurve.exists_variableChange_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E_1 E' : WeierstrassCurve F
inst_2 : E_1.IsElliptic
inst_3 : E'.IsElliptic
p : ℕ
inst_4 : CharP F p
hchar2 : Ne.{u_1 + 1} (α := F) 2 0
hchar3 : Ne.{u_1 + 1} (α := F) 3 0
this_1 : NeZero.{u_1} (R := F) 2
this_2 : NeZero.{u_1} (R := F) 4
this_3 : NeZero.{u_1} (R := F) 6
this_4 : Invertible (α := F) 2 := invertibleOfNonzero hchar2
this_5 : Invertible (α := F) 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst_5 : E.IsElliptic
heq : E.j = E'.j
h : E.IsShortNF
this :
  ∀ (E' : WeierstrassCurve F) [inst_6 : E'.IsElliptic] (heq : E.j = E'.j) (h : E'.IsShortNF),
    ∃ (C : VariableChange F), C • E = E'
h_1 : ¬E'.IsShortNF
C : VariableChange F
hE' : (C • E').IsShortNF
⊢ E.j = (C • E').j

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

Premises used: WeierstrassCurve.variableChange_j