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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ (have this := ⋯;
    complEDS' b c d k ((2 * m + 1) / 2 + 1) ^ 2 * normEDS b c d ((↑((2 * m + 1) / 2 + 1) + 1) * k + 1) *
        normEDS b c d ((↑((2 * m + 1) / 2 + 1) + 1) * k - 1) -
      complEDS' b c d k ((2 * m + 1) / 2 + 1 + 1) ^ 2 * normEDS b c d (↑((2 * m + 1) / 2 + 1) * k + 1) *
        normEDS b c d (↑((2 * m + 1) / 2 + 1) * k - 1)) =
    complEDS' b c d k (m + 1) ^ 2 * normEDS b c d ((↑m + 2) * k + 1) * normEDS b c d ((↑m + 2) * k - 1) -
      complEDS' b c d k (m + 2) ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ (have this := ⋯;
    complEDS' b c d k ((2 * m + 1) / 2 + 1) ^ 2 * normEDS b c d ((↑((2 * m + 1) / 2 + 1) + 1) * k + 1) *
        normEDS b c d ((↑((2 * m + 1) / 2 + 1) + 1) * k - 1) -
      complEDS' b c d k ((2 * m + 1) / 2 + 1 + 1) ^ 2 * normEDS b c d (↑((2 * m + 1) / 2 + 1) * k + 1) *
        normEDS b c d (↑((2 * m + 1) / 2 + 1) * k - 1)) =
    complEDS' b c d k (m + 1) ^ 2 * normEDS b c d ((↑m + 2) * k + 1) * normEDS b c d ((↑m + 2) * k - 1) -
      complEDS' b c d k (m + 2) ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : IsAffine c.pt
⊢ ∃ i, IsAffine (D.obj i)

Tactic:
by
  have := isAffineHom_π_app _ _ hc
  obtain ⟨i, hi⟩ := Scheme.exists_isQuasiAffine_of_isLimit D c hc
  have : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f) := by
    dsimp; infer_instance
  have (j : _) : CompactSpace ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j) := by dsimp; infer_instance
  obtain ⟨j, fij, hj⟩ := exists_map_eq_top _ _
    (isLimitOfPreserves (Scheme.Γ.rightOp ⋙ Scheme.Spec) hc) (D.obj i).toSpecΓ.opensRange
    ((preimage_opensRange_toSpecΓ (X := c.pt) (c.π.app i)).trans
      (by simp [Hom.opensRange_of_isIso]))
  have := IsQuasiAffine.of_isAffineHom (D.map fij)
  exact ⟨j, ⟨isIso_of_isOpenImmersion_of_opensRange_eq_top _
    ((preimage_opensRange_toSpecΓ (D.map fij)).symm.trans hj)⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

Tactic:
]

Goal state after:
case neg
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

Tactic:
]

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

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      f (preNormEDS' b c d (m✝ + 1)) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      f (preNormEDS' b c d (m✝ + 1)) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some
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
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • some dp) (2 • some dq + 3)

Tactic:
]

Goal state after:
case neg.some.some
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
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • some dp) (2 • some dq + 3)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * f (preNormEDS' b c d (m✝ + 2)) ^ 3 * if Even m✝ then f b else 1) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b

Tactic:
]

Goal state after:
case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * f (preNormEDS' b c d (m✝ + 2)) ^ 3 * if Even m✝ then f b else 1) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b

Tactic:
]

Goal state after:
case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b

Tactic:
]

Goal state after:
case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * f (preNormEDS' b c d (m✝ + 3)) ^ 3 * if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e'_3.e'_4
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 dq + 3 = 2 • some dq + 3

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case intro.refine_2
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k✝ : I
fkj : k✝ ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
k : J
⊢ c.π.app (j k) ⁻¹ᵁ V k = c.π.app (j k) ⁻¹ᵁ V k

Tactic:
]

Goal state after:
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

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
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ ((preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 *
        if Even m✝ then 1 else f b) =
    (preNormEDS' (f b) (f c) (f d) (m✝ + 4) * preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 3 * if Even m✝ then f b else 1) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) ^ 3 * if Even m✝ then 1 else f b

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
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

Tactic:
]

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
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_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.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1), f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ complEDS' (f b) (f c) (f d) k (m✝ + 1) * complEDS₂ (f b) (f c) (f d) ((↑m✝ + 1) * k) =
    complEDS' (f b) (f c) (f d) k (m✝ + 1) * complEDS₂ (f b) (f c) (f d) ((↑m✝ + 1) * k)

Tactic:
]

Goal state after: