-- Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean
theorem exists_variableChange_of_j_eq (heq : E.j = E'.j) :
    ∃ C : VariableChange F, E.variableChange C = E'

Proof state:
case neg
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
hchar3 : ¬p = 3
⊢ ∃ C, E.variableChange C = E'

Tactic:
exact exists_variableChange_of_char_ne_two_or_three _ _ hchar2 hchar3 heq

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
heq : E.j = E'.j
⊢ ∃ C, E.variableChange C = E'

Tactic:
obtain ⟨p, _⟩ := CharP.exists F

Result:
case intro
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
⊢ ∃ C, E.variableChange C = E'

Proof state:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
hchar3 : p = 3
⊢ ∃ C, E.variableChange C = E'

Tactic:
subst hchar3

Result:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
h✝ : CharP F 3
hchar2 : ¬3 = 2
⊢ ∃ 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
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
⊢ ∃ C, E.variableChange C = E'

Tactic:
by_cases hchar2 : p = 2

Result:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : p = 2
⊢ ∃ C, E.variableChange C = E'

case neg
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
⊢ ∃ C, E.variableChange C = E'

Proof state:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
h✝ : CharP F 3
hchar2 : ¬3 = 2
⊢ ∃ C, E.variableChange C = E'

Tactic:
exact exists_variableChange_of_char_three _ _ heq

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
⊢ ∃ C, E.variableChange C = E'

Tactic:
by_cases hchar3 : p = 3

Result:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
hchar3 : p = 3
⊢ ∃ C, E.variableChange C = E'

case neg
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
hchar3 : ¬p = 3
⊢ ∃ C, E.variableChange C = E'

Proof state:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : p = 2
⊢ ∃ C, E.variableChange C = E'

Tactic:
subst hchar2

Result:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
h✝ : CharP F 2
⊢ ∃ C, E.variableChange C = E'

Proof state:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
h✝ : CharP F 2
⊢ ∃ C, E.variableChange C = E'

Tactic:
exact exists_variableChange_of_char_two _ _ heq

Result:
no goals