mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «0»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ ((-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * x 0 ^ 2 +
                  (2 * W.b₂ * W.b₄ * W.b₈ - 2 * W.b₄ ^ 2 * W.b₆ - 10 * W.b₆ * W.b₈) * x 0 * x 1 +
                (-(W.b₂ * W.b₆ * W.b₈) + W.b₄ * W.b₆ ^ 2) * x 0 * x 2 +
              (3 * W.b₄ ^ 2 * W.b₈ - 3 * W.b₄ * W.b₆ ^ 2) * x 1 ^ 2 +
            (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * x 1 * x 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        ((-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * x 0 ^ 2 +
                  (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * x 0 * x 1 +
                (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * x 0 * x 2 +
              (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * x 1 ^ 2 +
            (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * x 1 * x 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      ((W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * x 0 ^ 2 +
            (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * x 0 * x 1 +
          (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * x 0 * x 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 0 ^ 4

Tactic:
grind only [b_relation]

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ (96 * W.b₆ * x 0 * x 1 + (12 * W.b₂ * W.b₆ - 64 * W.b₈) * x 1 ^ 2 + 16 * W.b₄ * W.b₆ * x 1 * x 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        (-(48 * W.b₆ * x 0 ^ 2) + 32 * W.b₈ * x 0 * x 1 + (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * x 1 ^ 2 +
            16 * W.b₄ * W.b₈ * x 1 * x 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      (-(12 * W.b₂ * W.b₆ * x 0 ^ 2) + (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * x 0 * x 1 + -(12 * W.b₆ ^ 2 * x 0 * x 2) +
            (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * x 1 ^ 2 +
          (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * x 1 * x 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 1 ^ 4

Tactic:
grind only [b_relation]

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

Goal state before:
pp: case «2»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ (-(12 * x 1 ^ 2) + -(4 * W.b₂ * x 1 * x 2) + (W.b₂ ^ 2 - 32 * W.b₄) * x 2 ^ 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        (6 * x 0 * x 1 + -(W.b₂ * x 0 * x 2) + -(5 * W.b₄ * x 1 * x 2) + (W.b₂ * W.b₄ - 27 * W.b₆) * x 2 ^ 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      (-(8 * W.b₄ * x 0 * x 2) + -(12 * W.b₆ * x 1 * x 2) + (W.b₄ ^ 2 - 28 * W.b₈) * x 2 ^ 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 2 ^ 4

Tactic:
grind only [b_relation]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ (2 * ↑(expDegree (2 * m + 6)) = 2 * (2 * ↑(expDegree (m + 2))) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      2 * ↑(expDegree (2 * m + 6)) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (2 * ↑(expDegree (m + 2))) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (2 * ↑(expDegree (m + 2))) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (2 * ↑(expDegree (m + 2))) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
have 𝒰 := (c.pt.isBasis_affineOpens).isOpenCover_mem_and_le
    (((X.isBasis_affineOpens).isOpenCover_mem_and_le
    ((S.isBasis_affineOpens).isOpenCover.comap f.base.hom)).comap a.base.hom)

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (2 * ↑(expDegree (m + 2))) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (2 * ↑(expDegree (m + 2))) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    ((↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
rw [expDegree_cast <| by lia]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    ((↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u • P ≈ v • Q ↔ P ≈ Q

Tactic:
← Quotient.eq_iff_equiv,

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦u • P⟧ = ⟦v • Q⟧ ↔ P ≈ Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦u • P⟧ = ⟦v • Q⟧ ↔ P ≈ Q

Tactic:
← Quotient.eq_iff_equiv,

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦u • P⟧ = ⟦v • Q⟧ ↔ ⟦P⟧ = ⟦Q⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomial = 0 ↔
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
      0

Tactic:
eval_polynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
      0 ↔
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
      0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
⊢ E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0

Tactic:
exact ⟨ha₄, ha₄'⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
⊢ E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0

Tactic:
exact ⟨ha₄, ha₄'⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
hu6 : u ^ 6 = E.a₆ / E'.a₆
⊢ E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0

Tactic:
exact ⟨ha₄, ha₄'⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ ↑x ≠ 0

Tactic:
have := x.prop

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
this : ↑x ∈ posSubmonoid R
⊢ ↑x ≠ 0
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' (𝓝 0 ⊓ 𝓝 y) = ⊥

Tactic:
rw [eq_bot]

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' ⊥ = ⊥
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
hasup : a ∈ I ⊔ span {a}
⊢ i ∈ span {x * y}

Tactic:
rw [hx, mem_span_singleton'] at hisup hasup

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
hisup : ∃ a, a * x = i
hasup : ∃ a_1, a_1 * x = a
⊢ i ∈ span {x * y}
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
⊢ u * x ∈ span {x * y}

Tactic:
obtain ⟨z, rfl⟩ : ∃ z, z * y = u := by
        rw [← mem_span_singleton', ← hy, mem_colon_span_singleton, mul_comm v, ← mul_assoc]
        exact mul_mem_right _ _ hi

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
z : R
hi : z * y * x ∈ I
⊢ z * y * x ∈ span {x * y}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addY P P = 0

Tactic:
rw [addY, negY_eq, addX_self hP, negAddY_self, addZ_self]
  ring1

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R✝ : Type u_1
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
x : (ofClass Valued.v).ValueGroup₀
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) ((WithZero.map' ↑(valueGroupEquiv v)) x) = x

Tactic:
by
    match x with
    | 0 => simp
    | .coe a => simp

Goal state after: