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

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.114} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.114} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := ⋯
xj : ↥(d.cover.X j) := ⋯
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 : (trans 𝒰 fi) uk = (d.natTrans.app i) xi
h2 : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
⊢ (𝒰.f j) ((d.natTrans.app j) xj) = (𝒰.f j) (((functorOfLocallyDirected 𝒰).map fj) uk)

Tactic:
dsimp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.114} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.114} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := (pullback.fst (d.cover.f i) (d.cover.f j)) x
xj : ↥(d.cover.X j) := (pullback.snd (d.cover.f i) (d.cover.f j)) x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 : (trans 𝒰 fi) uk = (d.natTrans.app i) xi
h2 : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
⊢ (𝒰.f j) ((d.natTrans.app j) xj) = (𝒰.f j) ((trans 𝒰 fj) uk)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
i : ℕ
hi : f.natDegree < i
⊢ f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)

Tactic:
· exact ⟨f.natDegree + 1, by simp, by simp [f.coeff_eq_zero_of_natDegree_lt hi]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰 : PreZeroHypercover S
𝒱 : PreZeroHypercover S
f : 𝒱.Hom 𝒰
inst✝ : QuasiCompactCover 𝒱
U : S.Opens
hU : IsAffineOpen U
i : 𝒱.I₀
⊢ ∀ (x : ↥(𝒱.X i)), (𝒱.f i) x = (⇑(𝒰.f (f.s₀ i)) ∘ ⇑(f.h₀ i)) x

Tactic:
by simp [← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
𝒰 : Cover (precoverage P) S
i : 𝒰.I₀
y : ↥(𝒰.X i)
⊢ ({ I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.f default) ((Sigma.ι 𝒰.X i) y) = (𝒰.f i) y

Tactic:
by simp [← Scheme.Hom.comp_apply]

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.b₄ = W.a₁ * W.a₃

Tactic:
rw [b₄]
  linear_combination W.a₄ * 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✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).Δ' = (Units.map ↑f) W.Δ'

Tactic:
by
  ext
  exact W.coe_map_Δ' f

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

Goal state before:
pp: case succ
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
⊢ ∃ T,
    comap MvPolynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 1) ∧
          ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 1)

Tactic:
| succ n IH =>

Goal state after:
case succ
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
⊢ ∃ T,
    comap MvPolynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 1) ∧
          ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 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)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0

Tactic:
have : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i))) :=
    isCompact_iff_compactSpace.mp (by simpa)

Goal state after:
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)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hx : x₁ = x₂
⊢ (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
        (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆ + (y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂)) -
      (0 + (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ + (x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆))) =
    0

Tactic:
(rw [hx]; ring1)

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
x : R[X][Y]
⊢ (AdjoinRoot.lift ((AdjoinRoot.of (W'.map f).polynomial).comp (mapRingHom f)) (AdjoinRoot.root (W'.map f).polynomial)
        ⋯)
      ((mk W') x) =
    (mk (W'.map f)) (Polynomial.map (mapRingHom f) x)

Tactic:
AdjoinRoot.lift_mk,

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x : R[X][Y]
⊢ eval₂ ((AdjoinRoot.of (W'.map f).polynomial).comp (mapRingHom f)) (AdjoinRoot.root (W'.map f).polynomial) x =
    (mk (W'.map f)) (Polynomial.map (mapRingHom f) x)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ XYIdeal W' x (C y) = XYIdeal W' x (linePolynomial x y ℓ)

Tactic:
by
  simp only [XYIdeal, XClass, YClass, linePolynomial]
  rw [← span_pair_add_left_mul _ _ <| mk W' <| C <| C <| -ℓ, ← map_mul, ← map_add]
  congr 4
  C_simp
  ring1

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ span {XClass W x, YClass W (C (W.negY x y))} * span {XClass W x, YClass W (C y)} = XIdeal W x

Tactic:
XClass,

Goal state after:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ span {(mk W) (C (X - C x)), YClass W (C (W.negY x y))} * span {(mk W) (C (X - C x)), YClass W (C y)} = XIdeal W x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e'_2.e'_5
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 {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)}) = ⊤

Tactic:
XClass,

Goal state after:
case e'_2.e'_5
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 (X - C x₁))} ⊔ (span {(mk W) (C (X - C x₂))} ⊔ span {(mk W) (Y - W.negPolynomial)}) = ⊤
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (if hn : Even (2 * m + 1) then
      (preNormEDS' b c d ((2 * m + 1) / 2 + 4) * preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 3 *
          if Even ((2 * m + 1) / 2) then b else 1) -
        preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) ^ 3 *
          if Even ((2 * m + 1) / 2) then 1 else b
    else
      have this := ⋯;
      preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
          preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
        preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
          preNormEDS' b c d ((2 * m + 1) / 2 + 4) ^ 2) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Tactic:
dif_neg m.not_even_two_mul_add_one

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (have this := ⋯;
    preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
      preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 4) ^ 2) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ (if hn : Even (2 * m + 1) then complEDS' b c d k ((2 * m + 1) / 2 + 1) * complEDS₂ b c d (↑((2 * m + 1) / 2 + 1) * k)
    else
      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:
dif_neg m.not_even_two_mul_add_one

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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
⊢ ∃ i R f,
    ∃ (_ : Presieve.ofArrows (fun i ↦ Spec (R i)) f ∈ zariskiPrecoverage.coverings (D.obj i)),
      ∃ g, ∀ (j : 𝒰.I₀), IsPullback (g j) (𝒰.f j) (f j) (c.π.app i)

Tactic:
have hV'' (k) := dsimp% congr($((hV' k).right).carrier)

Goal state after:
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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
⊢ ∃ i R f,
    ∃ (_ : Presieve.ofArrows (fun i ↦ Spec (R i)) f ∈ zariskiPrecoverage.coverings (D.obj i)),
      ∃ g, ∀ (j : 𝒰.I₀), IsPullback (g j) (𝒰.f j) (f j) (c.π.app i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

Tactic:
ΨSq,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ (W.preΨ (2 * m) ^ 2 * if Even (2 * m) then W.Ψ₂Sq else 1) =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

Tactic:
ΨSq,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ (W.preΨ (2 * m + 1) ^ 2 * if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
    ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^
      2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (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:
convert!
              (degree_sub_eq_left_of_degree_lt <|
                    (degree_add_le _ _).trans_lt <|
                      max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
                (max_eq_left_of_lt _).symm <;> rw [hdp] <;>
                exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

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

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

Tactic:
ΨSq,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C (W.preΨ n) * if Even n then W.ψ₂ else 1) ^ 2 = (mk W) (C (W.preΨ n ^ 2 * if Even n then W.Ψ₂Sq else 1))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (W.ψ n) = (mk W) (W.Ψ n)

Tactic:
simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 4 = C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Tactic:
rw [φ, ψ_four, show (4 + 1 : ℤ) = 2 * 2 + 1 by rfl, ψ_odd, two_add_two_eq_four, ψ_four,
    show (2 - 1 : ℤ) = 1 by rfl, ψ_two, ψ_one, two_add_one_eq_three, show (4 - 1 : ℤ) = 3 by rfl,
    ψ_three]

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * C W.Ψ₃ ^ 3) * C W.Ψ₃ =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
Q : W'.Point
⊢ zero.sym2x Q ≠ 0

Tactic:
cases Q

Goal state after:
case zero.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ zero.sym2x zero ≠ 0

case zero.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
Q : W'.Point
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x Q ≠ 0

Tactic:
cases Q

Goal state after:
case some.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero ≠ 0

case some.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
Q : W'.Point
⊢ zero.sym2x Q = Q.sym2x zero

Tactic:
cases Q

Goal state after:
case zero.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
⊢ zero.sym2x zero = zero.sym2x zero

case zero.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x zero
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
Q : W'.Point
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x Q = Q.sym2x (some x✝ y✝ h✝)

Tactic:
cases Q

Goal state after:
case some.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero = zero.sym2x (some x✝ y✝ h✝)

case some.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x (some x✝¹ y✝¹ h✝¹)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)

Tactic:
simp [ΨSq, ← coe_mapRingHom, apply_ite <| mapRingHom f]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -1 ^ 3 - 864 * W.a₆ = 1

Tactic:
linear_combination (-1 - 432 * W.a₆) * CharP.cast_eq_zero R 2

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

Goal state before:
pp: case odd.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
⊢ ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2).natDegree ≤
    expDegree (2 * (m + 2) + 1)

Tactic:
nth_rw 1 [← max_self <| expDegree _, (expDegree_rec m).2.1, (expDegree_rec m).2.2]
      refine natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp h₃.1)) ?_) <;>
        split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3) / P z ^ 3 + (W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * 1) -
      (Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialY +
        (W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * (P z ^ 3 / P z ^ 3))) =
    0

Tactic:
Affine.evalEval_polynomialY

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3) / P z ^ 3 + (W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * 1) -
      (2 * (P y / P z ^ 3) + W.toAffine.a₁ * (P x / P z ^ 2) + W.toAffine.a₃ +
        (W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * (P z ^ 3 / P z ^ 3))) =
    0