mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
⊢ Nonempty ↥c.pt

Tactic:
let F := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget _

Goal state after:
case inr
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget (𝒰.X j)
⊢ Nonempty ↥c.pt
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✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁ : (D.map k.hom) ((D.map (Over.Hom.left f)) x) ∈ U
h₂ : ⟨(D.map (Over.Hom.left f)) x, h₁⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base)
      ⟨(D.map (Over.Hom.left f)) x, h₁⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U

Tactic:
dsimp at h₁

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✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁ : (D.map k.hom) ((D.map (Over.Hom.left f)) x) ∈ U
h₂ : ⟨(D.map (Over.Hom.left f)) x, h₁⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base)
      ⟨(D.map (Over.Hom.left f)) x, h₁⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: S : Scheme
X : Over S
𝒰 : X.left.OpenCover
inst✝¹ : Category.{v_2, u_1} 𝒰.I₀
inst✝ : Cover.LocallyDirected 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
i : 𝒰.I₀
⊢ 𝒰.f i ≫ Over.Hom.left (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w) = g i

Tactic:
simp [glueMorphismsOverOfLocallyDirected]

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case h
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
y : ↥(d.functor.obj i)
⊢ (𝒰.f i) ((d.natTrans.app i) y) = (colimit.ι d.functor i ≫ d.toBase) y

Tactic:
ι_toBase

Goal state after:
case h
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
y : ↥(d.functor.obj i)
⊢ (𝒰.f i) ((d.natTrans.app i) y) = (d.natTrans.app i ≫ 𝒰.f i) y
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
inst✝ : Unique ι
x✝ : ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U
V : Opens (X default)
hc : IsCompact V.carrier
h : f default '' V.carrier = U
⊢ IsCompactOpenCovered f U

Tactic:
· refine ⟨{default}, Set.finite_singleton _, fun i h ↦ h ▸ V, fun i ↦ ?_, by simpa⟩
    rintro rfl
    simpa

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃.inl
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Subsingleton R
⊢ ∃ T,
    comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T, C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀ c ^ c.powBound

Tactic:
use ∅
      simp [ConstructibleSetData.toSet, Subsingleton.elim f 0]

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf✝ : ∀ (i : ι), Continuous (f i)
U : Set S
ho✝ : IsOpen U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map a t
hcomp : (fun x ↦ f x.fst x.snd) ∘ p = fun x ↦ g x.fst x.snd
hp : Continuous p
hf : Continuous fun p ↦ f p.fst p.snd
V : Opens ((i : σ) × Y i)
hV : IsCompact V.carrier
heq : (fun p ↦ g p.fst p.snd) '' V.carrier = U
K : Set ((i : ι) × X i)
hK : IsCompact K
ho : IsOpen K
hVK : p '' V.carrier ⊆ K
hKU : K ⊆ (fun p ↦ f p.fst p.snd) ⁻¹' U
⊢ U ⊆ (fun p ↦ f p.fst p.snd) '' { carrier := K, is_open' := ho }.carrier

Tactic:
rw [← heq, ← hcomp, Set.image_comp]

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf✝ : ∀ (i : ι), Continuous (f i)
U : Set S
ho✝ : IsOpen U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map a t
hcomp : (fun x ↦ f x.fst x.snd) ∘ p = fun x ↦ g x.fst x.snd
hp : Continuous p
hf : Continuous fun p ↦ f p.fst p.snd
V : Opens ((i : σ) × Y i)
hV : IsCompact V.carrier
heq : (fun p ↦ g p.fst p.snd) '' V.carrier = U
K : Set ((i : ι) × X i)
hK : IsCompact K
ho : IsOpen K
hVK : p '' V.carrier ⊆ K
hKU : K ⊆ (fun p ↦ f p.fst p.snd) ⁻¹' U
⊢ (fun x ↦ f x.fst x.snd) '' p '' V.carrier ⊆ (fun p ↦ f p.fst p.snd) '' { carrier := K, is_open' := ho }.carrier
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ y ^ 2 + (W.a₁ * x + W.a₃) * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) =
    y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)

Tactic:
rw [add_mul, ← add_assoc]

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY

Tactic:
slope_of_Y_ne hx hy,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x₁ y₁ x₂ ℓ : A
⊢ (W'⁄B).negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)

Tactic:
by
  rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
T : ConstructibleSetData (MvPolynomial (Fin n) R)
hT : comap MvPolynomial.C '' S'.toSet = T.toSet
hT' :
  ∀ C ∈ T,
    C.n ≤ MvPolynomialC.numBound (k + n) (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) m ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          Submodule.restrictScalars ℤ (degreesLE R (Fin n) Finset.univ.val) ^
            MvPolynomialC.degBound (k + n) (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) m
C : BasicConstructibleSetData (MvPolynomial (Fin n) R)
hCT : C ∈ T
i : Fin C.n
j : Fin n
⊢ degreeOf j (C.g i) ≤ degBound k m n d

Tactic:
have := (hT' C hCT).2 i
    rw [← Submodule.restrictScalars_pow (MvPolynomialC.degBound_pos ..).ne', ← degreesLE_nsmul,
      Submodule.restrictScalars_mem, mem_degreesLE,
        Multiset.le_iff_count] at this
    simpa only [Multiset.count_nsmul, Multiset.count_univ, mul_one, ← degreeOf_def]
      using! this j

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' h₁) * (ClassGroup.mk W.FunctionField) (XYIdeal' h₂) =
    (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯)

Tactic:
rw [← map_mul]
  exact (ClassGroup.mk_eq_mk_of_coe_ideal (coeIdeal_mul ..).symm <| XYIdeal'_eq _).mpr
    ⟨_, _, XClass_ne_zero _, YClass_ne_zero _, XYIdeal_mul_XYIdeal h₁.left h₂.left hxy⟩

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
show 4 = ((3 : ℕ) + 1 : ℤ) by rfl,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ (↑3 + 1) = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C X) * (mk W) (W.ψ n) ^ 2 - (mk W) (W.ψ (n + 1)) * (mk W) (W.ψ (n - 1)) =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * (mk W) (C (if Even n then 1 else W.Ψ₂Sq))

Tactic:
mk_ψ,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C X) * (mk W) (W.Ψ n) ^ 2 - (mk W) (W.Ψ (n + 1)) * (mk W) (W.Ψ (n - 1)) =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * (mk W) (C (if Even n then 1 else W.Ψ₂Sq))
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:
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.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:
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:
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:
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:
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:
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:
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