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

Proof state:
case intro.of_j_ne_zero.intro.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsShortNF
h : 0 ≠ 0
⊢ ∃ C, E.variableChange C = E'

Tactic:
exact False.elim (h rfl)

Result:
no goals

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
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (E.variableChange C).j = (E'.variableChange C').j
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : (E.variableChange C).variableChange C'' = E'.variableChange C'
⊢ E.variableChange ((C'.inv.comp C'').comp C) = E'

Tactic:
rw [variableChange_comp, variableChange_comp, hC, ← variableChange_comp,
  VariableChange.comp_left_inv, variableChange_id]

Result:
no goals

Proof state:
case intro.of_j_ne_zero.intro.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
⊢ ∃ C, E.variableChange C = E'

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

Result:
case intro.of_j_ne_zero.intro.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (E.variableChange C).j = (E'.variableChange C').j
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
⊢ ∃ C, E.variableChange C = E'

Proof state:
case intro.of_j_ne_zero.intro.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsShortNF
h : (E.variableChange C).j ≠ 0
⊢ ∃ C, E.variableChange C = E'

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

Result:
case intro.of_j_ne_zero.intro.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsShortNF
h : 0 ≠ 0
⊢ ∃ C, E.variableChange C = E'

Proof state:
case intro.of_j_eq_zero.intro.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsShortNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
h : 0 ≠ 0
⊢ ∃ C, E.variableChange C = E'

Tactic:
exact False.elim (h rfl)

Result:
no goals

Proof state:
case intro.of_j_ne_zero.intro.of_j_ne_zero.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
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (E.variableChange C).j = (E'.variableChange C').j
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : (E.variableChange C).variableChange C'' = E'.variableChange C'
⊢ ∃ C, E.variableChange C = E'

Tactic:
use (C'.inv.comp C'').comp C

Result:
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
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (E.variableChange C).j = (E'.variableChange C').j
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
C'' : VariableChange F
hC : (E.variableChange C).variableChange C'' = E'.variableChange C'
⊢ E.variableChange ((C'.inv.comp C'').comp C) = E'

Proof state:
case intro.of_j_ne_zero
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝³ : E.IsElliptic
inst✝² : E'.IsElliptic
inst✝¹ : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝ : (E.variableChange C).IsCharThreeJNeZeroNF
⊢ ∃ C, E.variableChange C = E'

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

Result:
case intro.of_j_ne_zero.intro.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
⊢ ∃ C, E.variableChange C = E'

case intro.of_j_ne_zero.intro.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsShortNF
⊢ ∃ C, E.variableChange C = E'

Proof state:
case intro.of_j_eq_zero
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝³ : E.IsElliptic
inst✝² : E'.IsElliptic
inst✝¹ : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝ : (E.variableChange C).IsShortNF
⊢ ∃ C, E.variableChange C = E'

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

Result:
case intro.of_j_eq_zero.intro.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsShortNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharThreeJNeZeroNF
⊢ ∃ C, E.variableChange C = E'

case intro.of_j_eq_zero.intro.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsShortNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsShortNF
⊢ ∃ C, E.variableChange C = E'

Proof state:
case intro.of_j_eq_zero.intro.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsShortNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsShortNF
⊢ ∃ C, E.variableChange C = E'

Tactic:
obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_eq_zero
  (E.variableChange C) (E'.variableChange C')

Result:
case intro.of_j_eq_zero.intro.of_j_eq_zero.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
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsShortNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsShortNF
C'' : VariableChange F
hC : (E.variableChange C).variableChange C'' = E'.variableChange C'
⊢ ∃ C, E.variableChange C = E'