mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case left
m : ℕ
⊢ 2 * (↑m + 3) / 2 =
    (((if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 2 * if Even m then ↑m + 3 else (↑m + 3) / 2) *
        if Even m then ↑m + 5 else (↑m + 5) / 2) -
      ((if Even m then ↑m + 1 else (↑m + 1) / 2) * if Even m then ↑m + 3 else (↑m + 3) / 2) *
        (if Even m then (↑m + 4) / 2 else ↑m + 4) ^ 2

pp: case right
m : ℕ
⊢ 2 * (↑m + 2) + 1 =
    ((if Even m then (↑m + 4) / 2 else ↑m + 4) * (if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 3 *
        if Even m then 16 else 1) -
      (if Even m then ↑m + 1 else (↑m + 1) / 2) * (if Even m then ↑m + 3 else (↑m + 3) / 2) ^ 3 *
        if Even m then 1 else 16

Tactic:
<;>

Goal state after:
case left
m : ℕ
⊢ 2 * (↑m + 3) / 2 =
    (((if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 2 * if Even m then ↑m + 3 else (↑m + 3) / 2) *
        if Even m then ↑m + 5 else (↑m + 5) / 2) -
      ((if Even m then ↑m + 1 else (↑m + 1) / 2) * if Even m then ↑m + 3 else (↑m + 3) / 2) *
        (if Even m then (↑m + 4) / 2 else ↑m + 4) ^ 2

case right
m : ℕ
⊢ 2 * (↑m + 2) + 1 =
    ((if Even m then (↑m + 4) / 2 else ↑m + 4) * (if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 3 *
        if Even m then 16 else 1) -
      (if Even m then ↑m + 1 else (↑m + 1) / 2) * (if Even m then ↑m + 3 else (↑m + 3) / 2) ^ 3 *
        if Even m then 1 else 16
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ 2 * (↑m + 3) / 2 = ((↑m + 2) / 2) ^ 2 * (↑m + 3) * (↑m + 5) - (↑m + 1) * (↑m + 3) * ((↑m + 4) / 2) ^ 2

pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ 2 * (↑m + 3) / 2 = (↑m + 2) ^ 2 * ((↑m + 3) / 2) * ((↑m + 5) / 2) - (↑m + 1) / 2 * ((↑m + 3) / 2) * (↑m + 4) ^ 2

pp: case pos
m : ℕ
h✝ : Even m
⊢ 2 * (↑m + 2) + 1 = (↑m + 4) / 2 * ((↑m + 2) / 2) ^ 3 * 16 - (↑m + 1) * (↑m + 3) ^ 3 * 1

pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ 2 * (↑m + 2) + 1 = (↑m + 4) * (↑m + 2) ^ 3 * 1 - (↑m + 1) / 2 * ((↑m + 3) / 2) ^ 3 * 16

Tactic:
<;>

Goal state after:
case pos
m : ℕ
h✝ : Even m
⊢ 2 * (↑m + 3) / 2 = ((↑m + 2) / 2) ^ 2 * (↑m + 3) * (↑m + 5) - (↑m + 1) * (↑m + 3) * ((↑m + 4) / 2) ^ 2

case neg
m : ℕ
h✝ : ¬Even m
⊢ 2 * (↑m + 3) / 2 = (↑m + 2) ^ 2 * ((↑m + 3) / 2) * ((↑m + 5) / 2) - (↑m + 1) / 2 * ((↑m + 3) / 2) * (↑m + 4) ^ 2

case pos
m : ℕ
h✝ : Even m
⊢ 2 * (↑m + 2) + 1 = (↑m + 4) / 2 * ((↑m + 2) / 2) ^ 3 * 16 - (↑m + 1) * (↑m + 3) ^ 3 * 1

case neg
m : ℕ
h✝ : ¬Even m
⊢ 2 * (↑m + 2) + 1 = (↑m + 4) * (↑m + 2) ^ 3 * 1 - (↑m + 1) / 2 * ((↑m + 3) / 2) ^ 3 * 16
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case «0»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨0, ⋯⟩) = P ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨1, ⋯⟩) = P ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨2, ⋯⟩) = P ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨0, ⋯⟩) = P ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨1, ⋯⟩) = P ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨2, ⋯⟩) = P ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case «0»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f ∘ (u • P)) ((fun i ↦ i) ⟨0, ⋯⟩) = (f u • ⇑f ∘ P) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f ∘ (u • P)) ((fun i ↦ i) ⟨1, ⋯⟩) = (f u • ⇑f ∘ P) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f ∘ (u • P)) ((fun i ↦ i) ⟨2, ⋯⟩) = (f u • ⇑f ∘ P) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f ∘ (u • P)) ((fun i ↦ i) ⟨0, ⋯⟩) = (f u • ⇑f ∘ P) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f ∘ (u • P)) ((fun i ↦ i) ⟨1, ⋯⟩) = (f u • ⇑f ∘ P) ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ (⇑f ∘ (u • P)) ((fun i ↦ i) ⟨2, ⋯⟩) = (f u • ⇑f ∘ P) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case «0»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨0, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨0, ⋯⟩

pp: case «1»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨1, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨1, ⋯⟩

pp: case «2»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨2, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨2, ⋯⟩

Tactic:
<;>

Goal state after:
case «0»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨0, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨0, ⋯⟩

case «1»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨1, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨1, ⋯⟩

case «2»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨2, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨2, ⋯⟩
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case of_j_eq_zero.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✝¹ : (C • E).IsShortNF
C' : VariableChange F
inst✝ : (C' • E').IsCharThreeJNeZeroNF
⊢ ∃ C, C • E = E'

pp: case of_j_eq_zero.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✝¹ : (C • E).IsShortNF
C' : VariableChange F
inst✝ : (C' • E').IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
· have h := (C' • E').j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
      rw [variableChange_j, ← heq, ← variableChange_j E C, j_of_isShortNF_of_char_three] at h
      exact False.elim (h rfl)

Goal state after:
case of_j_eq_zero.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✝¹ : (C • E).IsShortNF
C' : VariableChange F
inst✝ : (C' • E').IsShortNF
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case e'_3.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even (2 * n) then 2 * n / 2 else 2 * n) = ↑(expCoeff (2 * n))

pp: case e'_3.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) = ↑(expCoeff (2 * n + 1))

Tactic:
<;>

Goal state after:
case e'_3.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even (2 * n) then 2 * n / 2 else 2 * n) = ↑(expCoeff (2 * n))

case e'_3.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) = ↑(expCoeff (2 * n + 1))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
h✝ : Even n
⊢ 2 ≤ n ^ 2 - 4

pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
h✝ : ¬Even n
⊢ 2 ≤ n ^ 2 - 1

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
h✝ : Even n
⊢ 2 ≤ n ^ 2 - 4

case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
h✝ : ¬Even n
⊢ 2 ≤ n ^ 2 - 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
h : ↑0 ≠ 0
hn : ¬2 < 0
⊢ W.preΨ' 0 ≠ 0

pp: case neg.succ.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
h : ↑(0 + 1) ≠ 0
hn : ¬2 < 0 + 1
⊢ W.preΨ' (0 + 1) ≠ 0

pp: case neg.succ.succ
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n✝ : ℕ
h : ↑(n✝ + 1 + 1) ≠ 0
hn : ¬2 < n✝ + 1 + 1
⊢ W.preΨ' (n✝ + 1 + 1) ≠ 0

Tactic:
<;>

Goal state after:
case neg.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
h : ↑0 ≠ 0
hn : ¬2 < 0
⊢ W.preΨ' 0 ≠ 0

case neg.succ.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
h : ↑(0 + 1) ≠ 0
hn : ¬2 < 0 + 1
⊢ W.preΨ' (0 + 1) ≠ 0

case neg.succ.succ
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n✝ : ℕ
h : ↑(n✝ + 1 + 1) ≠ 0
hn : ¬2 < n✝ + 1 + 1
⊢ W.preΨ' (n✝ + 1 + 1) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
ih :
  (W.preΨ ↑(2 * n)).coeff (((↑(2 * n)).natAbs ^ 2 - if Even ↑(2 * n) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n) then ↑(2 * n) / 2 else ↑(2 * n))
⊢ -(W.preΨ ↑(2 * n)).coeff (((↑(2 * n)).natAbs ^ 2 - if Even ↑(2 * n) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n) then -↑(2 * n) / 2 else -↑(2 * n))

pp: case neg.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
ih :
  (W.preΨ ↑(2 * n + 1)).coeff (((↑(2 * n + 1)).natAbs ^ 2 - if Even ↑(2 * n + 1) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n + 1) then ↑(2 * n + 1) / 2 else ↑(2 * n + 1))
⊢ -(W.preΨ ↑(2 * n + 1)).coeff (((↑(2 * n + 1)).natAbs ^ 2 - if Even ↑(2 * n + 1) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n + 1) then -↑(2 * n + 1) / 2 else -↑(2 * n + 1))

Tactic:
<;>

Goal state after:
case neg.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
ih :
  (W.preΨ ↑(2 * n)).coeff (((↑(2 * n)).natAbs ^ 2 - if Even ↑(2 * n) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n) then ↑(2 * n) / 2 else ↑(2 * n))
⊢ -(W.preΨ ↑(2 * n)).coeff (((↑(2 * n)).natAbs ^ 2 - if Even ↑(2 * n) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n) then -↑(2 * n) / 2 else -↑(2 * n))

case neg.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
ih :
  (W.preΨ ↑(2 * n + 1)).coeff (((↑(2 * n + 1)).natAbs ^ 2 - if Even ↑(2 * n + 1) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n + 1) then ↑(2 * n + 1) / 2 else ↑(2 * n + 1))
⊢ -(W.preΨ ↑(2 * n + 1)).coeff (((↑(2 * n + 1)).natAbs ^ 2 - if Even ↑(2 * n + 1) then 4 else 1) / 2) =
    ↑(if Even ↑(2 * n + 1) then -↑(2 * n + 1) / 2 else -↑(2 * n + 1))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n)).coeff (((2 * ↑n).natAbs ^ 2 - 4) / 2) = ↑(2 * ↑n / 2)
⊢ -(W.preΨ (2 * ↑n)).coeff (((2 * ↑n).natAbs ^ 2 - 4) / 2) = -↑(2 * ↑n / 2)

pp: case neg.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n + 1)).coeff (((2 * ↑n + 1).natAbs ^ 2 - 1) / 2) = 2 * ↑n + 1
⊢ -(W.preΨ (2 * ↑n + 1)).coeff (((2 * ↑n + 1).natAbs ^ 2 - 1) / 2) = -(2 * ↑n + 1)

Tactic:
<;>

Goal state after:
case neg.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n)).coeff (((2 * ↑n).natAbs ^ 2 - 4) / 2) = ↑(2 * ↑n / 2)
⊢ -(W.preΨ (2 * ↑n)).coeff (((2 * ↑n).natAbs ^ 2 - 4) / 2) = -↑(2 * ↑n / 2)

case neg.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n + 1)).coeff (((2 * ↑n + 1).natAbs ^ 2 - 1) / 2) = 2 * ↑n + 1
⊢ -(W.preΨ (2 * ↑n + 1)).coeff (((2 * ↑n + 1).natAbs ^ 2 - 1) / 2) = -(2 * ↑n + 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
h✝ : Even n.succ
⊢ ↑n ^ 2 + 2 * ↑n * 1 = ↑n ^ 2 + 2 * ↑n * 1 + 1 - 4 + 3

pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
h✝ : ¬Even n.succ
⊢ ↑n ^ 2 + 2 * ↑n * 1 = ↑n ^ 2 + 2 * ↑n * 1 + 1 - 1 + 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
h✝ : Even n.succ
⊢ ↑n ^ 2 + 2 * ↑n * 1 = ↑n ^ 2 + 2 * ↑n * 1 + 1 - 4 + 3

case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
h✝ : ¬Even n.succ
⊢ ↑n ^ 2 + 2 * ↑n * 1 = ↑n ^ 2 + 2 * ↑n * 1 + 1 - 1 + 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
h✝ : Even (n + 1)
⊢ (↑n + 1) ^ 2 = ((↑n + 1) / 2) ^ 2 * 4

pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
h✝ : ¬Even (n + 1)
⊢ (↑n + 1) ^ 2 = (↑n + 1) ^ 2 * 1

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
h✝ : Even (n + 1)
⊢ (↑n + 1) ^ 2 = ((↑n + 1) / 2) ^ 2 * 4

case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
h✝ : ¬Even (n + 1)
⊢ (↑n + 1) ^ 2 = (↑n + 1) ^ 2 * 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
h✝ : Even (n + 1)
⊢ W.Ψ₂Sq.natDegree ≤ 3

pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
h✝ : ¬Even (n + 1)
⊢ natDegree 1 ≤ 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
h✝ : Even (n + 1)
⊢ W.Ψ₂Sq.natDegree ≤ 3

case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
h✝ : ¬Even (n + 1)
⊢ natDegree 1 ≤ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : ¬1 < (↑(m + 1)).natAbs
hm : (↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq ↑(m + 1) ≠ 0

pp: case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : ¬1 < (-↑(m + 1)).natAbs
hm : (-↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq (-↑(m + 1)) ≠ 0

Tactic:
<;>

Goal state after:
case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : ¬1 < (↑(m + 1)).natAbs
hm : (↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq ↑(m + 1) ≠ 0

case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : ¬1 < (-↑(m + 1)).natAbs
hm : (-↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq (-↑(m + 1)) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq ↑(m + 1) ≠ 0

pp: case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq (-↑(m + 1)) ≠ 0

Tactic:
<;>

Goal state after:
case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq ↑(m + 1) ≠ 0

case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq (-↑(m + 1)) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
⊢ 1 ≠ 0

pp: case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
⊢ 1 ≠ 0

Tactic:
<;>

Goal state after:
case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
⊢ 1 ≠ 0

case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
⊢ 1 ≠ 0