-- Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean
private lemma exists_variableChange_of_char_three_of_j_eq_zero
    [E.IsShortNF] [E'.IsShortNF] :
    ∃ C : VariableChange F, E.variableChange C = E'

Proof state:
case h
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ E.variableChange { u := Units.mk0 u hu0, r := r, s := 0, t := 0 } = E'

Tactic:
ext

Result:
case h.a₁
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.variableChange { u := Units.mk0 u hu0, r := r, s := 0, t := 0 }).a₁ = E'.a₁

case h.a₂
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.variableChange { u := Units.mk0 u hu0, r := r, s := 0, t := 0 }).a₂ = E'.a₂

case h.a₃
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.variableChange { u := Units.mk0 u hu0, r := r, s := 0, t := 0 }).a₃ = E'.a₃

case h.a₄
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.variableChange { u := Units.mk0 u hu0, r := r, s := 0, t := 0 }).a₄ = E'.a₄

case h.a₆
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.variableChange { u := Units.mk0 u hu0, r := r, s := 0, t := 0 }).a₆ = E'.a₆

Proof state:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
⊢ ∃ C, E.variableChange C = E'

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

Result:
case intro
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
⊢ ∃ C, E.variableChange C = E'

Proof state:
case intro
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
⊢ ∃ C, E.variableChange C = E'

Tactic:
obtain ⟨r, hr⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 3 3
  1 _ (E.a₆ - u ^ 6 * E'.a₆) (by norm_num) (by norm_num) ha₄

Result:
case intro.intro
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
⊢ ∃ C, E.variableChange C = E'

Proof state:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
⊢ u ≠ 0

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

Result:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
⊢ E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0

Proof state:
case h.a₄
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.a₄ - 0 * 0 + 2 * r * 0 - (0 + r * 0) * 0 + 0 * r ^ 2 - 2 * 0 * 0) / (E.a₄ / E'.a₄) = E'.a₄

Tactic:
field_simp

Result:
no goals

Proof state:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
⊢ 2 ≤ 3

Tactic:
norm_num

Result:
no goals