mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        1 *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * 1) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * b) -
      preNormEDS (b ^ 4) c d (k - 2) * b * (preNormEDS (b ^ 4) c d (k + 1) * 1) ^ 2

pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : ¬Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * b) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * 1) -
      preNormEDS (b ^ 4) c d (k - 2) * 1 * (preNormEDS (b ^ 4) c d (k + 1) * b) ^ 2

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        1 *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * 1) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * b) -
      preNormEDS (b ^ 4) c d (k - 2) * b * (preNormEDS (b ^ 4) c d (k + 1) * 1) ^ 2

case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : ¬Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * b) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * 1) -
      preNormEDS (b ^ 4) c d (k - 2) * 1 * (preNormEDS (b ^ 4) c d (k + 1) * b) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * b ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * 1) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * b * (preNormEDS (b ^ 4) c d m * b) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * 1 * (preNormEDS (b ^ 4) c d (m + 1) * 1) ^ 3

pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * 1 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * b ^ 4) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * 1 * (preNormEDS (b ^ 4) c d m * 1) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * b * (preNormEDS (b ^ 4) c d (m + 1) * b) ^ 3

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * b ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * 1) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * b * (preNormEDS (b ^ 4) c d m * b) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * 1 * (preNormEDS (b ^ 4) c d (m + 1) * 1) ^ 3

case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * 1 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * b ^ 4) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * 1 * (preNormEDS (b ^ 4) c d m * 1) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * b * (preNormEDS (b ^ 4) c d (m + 1) * b) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inl.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < 2 • some dq + 3

pp: case neg.some.some.inl.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ some dp + some dq + 1 < 2 • some dq + 3

pp: case neg.some.some.inl.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < 2 • some dq + 3

Tactic:
<;>

Goal state after:
case neg.some.some.inl.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < 2 • some dq + 3

case neg.some.some.inl.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ some dp + some dq + 1 < 2 • some dq + 3

case neg.some.some.inl.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < 2 • some dq + 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ C (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) * W.ψ₂ * W.ψ₂ =
    (C (W.preΨ (m - 1)) * 1) ^ 2 * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 2)) * W.ψ₂) -
      C (W.preΨ (m - 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 1)) * 1) ^ 2

pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ C (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) * W.ψ₂ * W.ψ₂ =
    (C (W.preΨ (m - 1)) * W.ψ₂) ^ 2 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 2)) * 1) -
      C (W.preΨ (m - 2)) * 1 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 2

Tactic:
<;>

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ C (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) * W.ψ₂ * W.ψ₂ =
    (C (W.preΨ (m - 1)) * 1) ^ 2 * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 2)) * W.ψ₂) -
      C (W.preΨ (m - 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 1)) * 1) ^ 2

case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ C (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) * W.ψ₂ * W.ψ₂ =
    (C (W.preΨ (m - 1)) * W.ψ₂) ^ 2 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 2)) * 1) -
      C (W.preΨ (m - 2)) * 1 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m - 1)) ^ 2 * C (W.preΨ m) * C (W.preΨ (m + 2)) -
          C (W.preΨ (m - 2)) * C (W.preΨ m) * C (W.preΨ (m + 1)) ^ 2) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ (m - 1)) * 1) ^ 2 * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 2)) * W.ψ₂) -
      C (W.preΨ (m - 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 1)) * 1) ^ 2

pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m - 1)) ^ 2 * C (W.preΨ m) * C (W.preΨ (m + 2)) -
          C (W.preΨ (m - 2)) * C (W.preΨ m) * C (W.preΨ (m + 1)) ^ 2) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ (m - 1)) * W.ψ₂) ^ 2 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 2)) * 1) -
      C (W.preΨ (m - 2)) * 1 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 2

Tactic:
<;>

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m - 1)) ^ 2 * C (W.preΨ m) * C (W.preΨ (m + 2)) -
          C (W.preΨ (m - 2)) * C (W.preΨ m) * C (W.preΨ (m + 1)) ^ 2) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ (m - 1)) * 1) ^ 2 * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 2)) * W.ψ₂) -
      C (W.preΨ (m - 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 1)) * 1) ^ 2

case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m - 1)) ^ 2 * C (W.preΨ m) * C (W.preΨ (m + 2)) -
          C (W.preΨ (m - 2)) * C (W.preΨ m) * C (W.preΨ (m + 1)) ^ 2) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ (m - 1)) * W.ψ₂) ^ 2 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 2)) * 1) -
      C (W.preΨ (m - 2)) * 1 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inr.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ some dp + some dq + 1 < 2 • some dp

pp: case neg.some.some.inr.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp

pp: case neg.some.some.inr.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp

Tactic:
<;>

Goal state after:
case neg.some.some.inr.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ some dp + some dq + 1 < 2 • some dp

case neg.some.some.inr.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp

case neg.some.some.inr.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ C (W.preΨ (m + 2) * W.preΨ m ^ 3 * W.Ψ₂Sq ^ 2 - W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * 1) * 1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C (W.preΨ (m + 2) * W.preΨ m ^ 3)

pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ C (W.preΨ (m + 2) * W.preΨ m ^ 3 * 1 - W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * W.Ψ₂Sq ^ 2) * 1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C (-W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3)

Tactic:
<;>

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ C (W.preΨ (m + 2) * W.preΨ m ^ 3 * W.Ψ₂Sq ^ 2 - W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * 1) * 1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C (W.preΨ (m + 2) * W.preΨ m ^ 3)

case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ C (W.preΨ (m + 2) * W.preΨ m ^ 3 * 1 - W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * W.Ψ₂Sq ^ 2) * 1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C (-W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case none
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • none) (2 • q.degree + 3) ≠ 1

pp: case some.zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some 0) (2 • q.degree + 3) ≠ 1

pp: case some.succ.zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some (0 + 1)) (2 • q.degree + 3) ≠ 1

pp: case some.succ.succ
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ : ℕ
⊢ max (2 • some (n✝ + 1 + 1)) (2 • q.degree + 3) ≠ 1

Tactic:
<;>

Goal state after:
case none
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • none) (2 • q.degree + 3) ≠ 1

case some.zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some 0) (2 • q.degree + 3) ≠ 1

case some.succ.zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some (0 + 1)) (2 • q.degree + 3) ≠ 1

case some.succ.succ
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ : ℕ
⊢ max (2 • some (n✝ + 1 + 1)) (2 • q.degree + 3) ≠ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * C W.Ψ₂Sq ^ 2 - C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) * 1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)

pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 - C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * C W.Ψ₂Sq ^ 2) * 1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)

Tactic:
<;>

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * C W.Ψ₂Sq ^ 2 - C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) * 1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)

case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 - C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * C W.Ψ₂Sq ^ 2) * 1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 property✝ : p Point.zero
⊢ (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
        ⟨Point.zero, property✝⟩) =
    ⟨Point.zero, property✝⟩

pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
property✝ : p (Point.some x✝ y✝ h✝)
⊢ (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
        ⟨Point.some x✝ y✝ h✝, property✝⟩) =
    ⟨Point.some x✝ y✝ h✝, property✝⟩

Tactic:
<;>

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 property✝ : p Point.zero
⊢ (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
        ⟨Point.zero, property✝⟩) =
    ⟨Point.zero, property✝⟩

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
property✝ : p (Point.some x✝ y✝ h✝)
⊢ (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
        ⟨Point.some x✝ y✝ h✝, property✝⟩) =
    ⟨Point.some x✝ y✝ h✝, property✝⟩
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case none
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ (fun x ↦
        match x with
        | ⟨Point.zero, property⟩ => none
        | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
      ((fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) none) =
    none

pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
val✝ : { xy // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }
⊢ (fun x ↦
        match x with
        | ⟨Point.zero, property⟩ => none
        | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
      ((fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) (some val✝)) =
    some val✝

Tactic:
<;>

Goal state after:
case none
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ (fun x ↦
        match x with
        | ⟨Point.zero, property⟩ => none
        | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
      ((fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) none) =
    none

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
val✝ : { xy // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }
⊢ (fun x ↦
        match x with
        | ⟨Point.zero, property⟩ => none
        | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
      ((fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) (some val✝)) =
    some val✝