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

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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJNeZeroNF
⊢ ∃ C, E.variableChange C = E'

Tactic:
simp_rw [← variableChange_j E C, ← variableChange_j E' C',
  j_of_isCharTwoJNeZeroNF_of_char_two, one_div, inv_inj] 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 2
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJNeZeroNF
heq : (E.variableChange C).a₆ = (E'.variableChange C').a₆
⊢ ∃ 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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJEqZeroNF
⊢ ∃ C, E.variableChange C = E'

Tactic:
have h := (E.variableChange C).j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two

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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJEqZeroNF
h : (E.variableChange C).j ≠ 0
⊢ ∃ 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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJEqZeroNF
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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJEqZeroNF
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_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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJNeZeroNF
h : (E'.variableChange C').j ≠ 0
⊢ ∃ C, E.variableChange C = E'

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

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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJNeZeroNF
h : 0 ≠ 0
⊢ ∃ C, E.variableChange 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 2
heq : E.j = E'.j
C : VariableChange F
inst✝ : (E.variableChange C).IsCharTwoJNeZeroNF
⊢ ∃ C, E.variableChange C = E'

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

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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJNeZeroNF
⊢ ∃ 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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJEqZeroNF
⊢ ∃ 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 2
heq : E.j = E'.j
C : VariableChange F
inst✝ : (E.variableChange C).IsCharTwoJEqZeroNF
⊢ ∃ C, E.variableChange C = E'

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

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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJNeZeroNF
⊢ ∃ 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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (E.variableChange C).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (E'.variableChange C').IsCharTwoJEqZeroNF
⊢ ∃ C, E.variableChange C = E'

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