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

Goal state before:
pp: case refine_1.refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.252} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
⊢ ∀ (i : 𝒱.I₀),
    (((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
          pullback.fst s.pt.hom (𝒰.f i)) ≫
        Over.hom s.pt.toComma =
      𝒱.f i ≫ Over.hom d.glued.toComma

Tactic:
intro i

Goal state after:
case refine_1.refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.252} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i : 𝒱.I₀
⊢ (((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f i)) ≫
      Over.hom s.pt.toComma =
    𝒱.f i ≫ Over.hom d.glued.toComma
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
⊢ ∃ u, π.base ≫ u = f.base

Tactic:
apply IsRegularEpi.exists_of_isKernelPair _ (IsPullback.of_hasPullback _ _)

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
⊢ fst π.base π.base ≫ f.base = snd π.base π.base ≫ f.base
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
⊢ ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ u x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ u y

Tactic:
intro i

Goal state after:
case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i : 𝒰.I₀
⊢ ∀ (y : 𝒰.I₀), pullback.fst (𝒰.f i) (𝒰.f y) ≫ u i = pullback.snd (𝒰.f i) (𝒰.f y) ≫ u y
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_2
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
⊢ ∀ (x : (Precoverage.ZeroHypercover.pullback₁ π 𝒰).I₀),
    (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f x ≫ π ≫ Cover.glueMorphisms 𝒰 u ⋯ =
      (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f x ≫ f

Tactic:
intro i

Goal state after:
case refine_2
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i : (Precoverage.ZeroHypercover.pullback₁ π 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f i ≫ π ≫ Cover.glueMorphisms 𝒰 u ⋯ =
    (Precoverage.ZeroHypercover.pullback₁ π 𝒰).f i ≫ f
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.c₆ = W.a₁ ^ 6

Tactic:
by
  rw [c₆, b₂_of_char_two]
  linear_combination (18 * W.a₁ ^ 2 * W.b₄ - 108 * W.b₆ - W.a₁ ^ 6) * CharP.cast_eq_zero R 2

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.Δ = W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3

Tactic:
rw [Δ, b₂_of_char_two, b₄_of_char_two, b₆_of_char_two]

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ -(W.a₁ ^ 2) ^ 2 * W.b₈ - 8 * (W.a₁ * W.a₃) ^ 3 - 27 * (W.a₃ ^ 2) ^ 2 + 9 * W.a₁ ^ 2 * (W.a₁ * W.a₃) * W.a₃ ^ 2 =
    W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hmn
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
⊢ { val := y.g }.degBound ^ { val := y.g }.degBound ≤ S.degBound ^ S.degBound

Tactic:
by_cases h : S.degBound = 0

Goal state after:
case pos
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
h : S.degBound = 0
⊢ { val := y.g }.degBound ^ { val := y.g }.degBound ≤ S.degBound ^ S.degBound

case neg
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
h : ¬S.degBound = 0
⊢ { val := y.g }.degBound ^ { val := y.g }.degBound ≤ S.degBound ^ S.degBound
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
⊢ ∀ C ∈ Finset.biUnion S f, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
    intro x y hy hx
    have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
    refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
    gcongr
    · simpa [Submodule.one_eq_span]
    · refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
    · delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
y : W'.CoordinateRing
hy : (map W' f) y = 0
⊢ y = 0

Tactic:
obtain ⟨p, q, rfl⟩ := exists_smul_basis_eq y
    simp_rw [map_add, CoordinateRing.map_smul, map_one, map_mk, map_X] at hy
    obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy
    rw [Polynomial.map_eq_zero_iff hf] at hp hq
    simp_rw [hp, hq, zero_smul, add_zero]

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) = 0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ 2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
            (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
          (↑3 * W'.addX x₁ x₂ ℓ ^ (3 - 1) + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) +
        (0 + ℓ * 0) -
      (0 +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) +
          ℓ * (2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃)))) =
    0

Tactic:
(norm_num1; ring1)

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₂
⊢ ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ =
    ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) - W.a₂ -
          x₁ -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₂ - x₁) ^ 2

Tactic:
← neg_sub x₁,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ -(x₁ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
    -(x₁ -
            (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
              W.a₂)) -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (-(x₁ - x₂)) ^ 2
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.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span
            {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                  YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂ *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
C_addPolynomial,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span
            {(mk W)
                ((Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))))} ⊔
          span
            {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                  YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂ *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case left
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 := ⋯
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) := ⋯
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)) := ⋯
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) := ⋯
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
x : BasicConstructibleSetData (MvPolynomial (Fin m) R)
hx : x ∈ S
j : Fin x.n ⊕ Fin n
⊢ ∀ (i : Fin m →₀ ℕ),
    (MvPolynomial.coeff i
          (Sum.elim (⇑σ ∘ x.g) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))) j)).degrees ≤
      Finset.univ.val

Tactic:
intro i

Goal state after:
case left
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
x : BasicConstructibleSetData (MvPolynomial (Fin m) R)
hx : x ∈ S
j : Fin x.n ⊕ Fin n
i : Fin m →₀ ℕ
⊢ (MvPolynomial.coeff i
        (Sum.elim (⇑σ ∘ x.g) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))) j)).degrees ≤
    Finset.univ.val
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ W ((2 * ((a + b + (c + d)) / 2) - (d + c)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - c)).tdiv 2) *
          (W ((2 * ((a + b + (c + d)) / 2) - (b + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - b - ((a + b + (c + d)) / 2 - a)).tdiv 2)) -
        W ((2 * ((a + b + (c + d)) / 2) - (d + b)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - b)).tdiv 2) *
          (W ((2 * ((a + b + (c + d)) / 2) - (c + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - a)).tdiv 2)) +
      W ((2 * ((a + b + (c + d)) / 2) - (d + a)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - a)).tdiv 2) *
        (W ((2 * ((a + b + (c + d)) / 2) - (c + b)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - b)).tdiv 2)) =
    W ((a + b).tdiv 2) * W ((a - b).tdiv 2) * (W ((c + d).tdiv 2) * W ((c - d).tdiv 2)) -
        W ((a + c).tdiv 2) * W ((a - c).tdiv 2) * (W ((b + d).tdiv 2) * W ((b - d).tdiv 2)) +
      W ((a + d).tdiv 2) * W ((a - d).tdiv 2) * (W ((b + c).tdiv 2) * W ((b - c).tdiv 2))

Tactic:
Int.mul_ediv_cancel'

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ W ((a + b + (c + d) - (d + c)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - c)).tdiv 2) *
          (W ((a + b + (c + d) - (b + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - b - ((a + b + (c + d)) / 2 - a)).tdiv 2)) -
        W ((a + b + (c + d) - (d + b)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - b)).tdiv 2) *
          (W ((a + b + (c + d) - (c + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - a)).tdiv 2)) +
      W ((a + b + (c + d) - (d + a)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - a)).tdiv 2) *
        (W ((a + b + (c + d) - (c + b)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - b)).tdiv 2)) =
    W ((a + b).tdiv 2) * W ((a - b).tdiv 2) * (W ((c + d).tdiv 2) * W ((c - d).tdiv 2)) -
        W ((a + c).tdiv 2) * W ((a - c).tdiv 2) * (W ((b + d).tdiv 2) * W ((b - d).tdiv 2)) +
      W ((a + d).tdiv 2) * W ((a - d).tdiv 2) * (W ((b + c).tdiv 2) * W ((b - c).tdiv 2))

R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ 2 ∣ a + b + (c + d)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
a b c d : ℤ
⊢ f (atomRel W a b c d) = atomRel (⇑f ∘ W) a b c d

Tactic:
by
  simp_rw [atomRel, map_add, map_sub, map_mul, map_atom]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 1 + 2)) =
    preNormEDS b c d (↑m + 1 + 1) ^ 2 * preNormEDS b c d (↑m + 1 + 2) * preNormEDS b c d (↑m + 1 + 2 + 2) -
      preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 1 + 2) * preNormEDS b c d (↑m + 1 + 2 + 1) ^ 2

Tactic:
norm_cast

Goal state after:
case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d ↑(2 * (m + 1 + 2)) =
    preNormEDS b c d ↑(m + 1 + 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 2) * preNormEDS b c d ↑(m + 1 + 2 + 2) -
      preNormEDS b c d ↑(m + 1) * preNormEDS b c d ↑(m + 1 + 2) * preNormEDS b c d ↑(m + 1 + 2 + 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * (↑n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑n✝ + 1 + 1 + 2) * preNormEDS b c d (↑n✝ + 1 + 1) ^ 3 * if Even n✝ then b else 1) -
      preNormEDS b c d (↑n✝ + 1) * preNormEDS b c d (↑n✝ + 1 + 1 + 1) ^ 3 * if Even n✝ then 1 else b

Tactic:
norm_cast

Goal state after:
case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d ↑(2 * (n✝ + 1 + 1) + 1) =
    (preNormEDS b c d ↑(n✝ + 1 + 1 + 2) * preNormEDS b c d ↑(n✝ + 1 + 1) ^ 3 * if Even n✝ then b else 1) -
      preNormEDS b c d ↑(n✝ + 1) * preNormEDS b c d ↑(n✝ + 1 + 1 + 1) ^ 3 * if Even n✝ then 1 else b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: 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
⊢ (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:
by_cases hp : p = 0

Goal state after:
case pos
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 = 0
⊢ (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)

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 = 0
⊢ (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.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1)) = complEDS b c d k ↑(n✝ + 1) * complEDS₂ b c d (↑(n✝ + 1) * k)

Tactic:
norm_cast

Goal state after:
case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k ↑(2 * (n✝ + 1)) = complEDS b c d k ↑(n✝ + 1) * complEDS₂ b c d (↑(n✝ + 1) * k)