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

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

Tactic:
ring1

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

Goal state before:
pp: case h
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)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hxS : C ∈ S
j : Fin { f := e C.f, n := C.n, g := ⇑e ∘ C.g }.n
hj : j ∈ Finset.univ
⊢ ({ f := e C.f, n := C.n, g := ⇑e ∘ C.g }.g j).degree.succ ≤ 1 + Multiset.count 0 d

Tactic:
simp only [e, comp_apply]

Goal state after:
case h
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)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hxS : C ∈ S
j : Fin { f := e C.f, n := C.n, g := ⇑e ∘ C.g }.n
hj : j ∈ Finset.univ
⊢ ((MvPolynomial.finSuccEquiv R n) (C.g j)).degree.succ ≤ 1 + Multiset.count 0 d
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 * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)) =
    1 ^ 6 *
      (W.a₆ + { u := 1, r := x, s := 0, t := y }.r * W.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W.a₂ +
              { u := 1, r := x, s := 0, t := y }.r ^ 3 -
            { u := 1, r := x, s := 0, t := y }.t * W.a₃ -
          { u := 1, r := x, s := 0, t := y }.t ^ 2 -
        { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W.a₁)

Tactic:
ring1

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

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

Tactic:
ring1

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

Goal state before:
pp: case e'_1
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ 2 * y + W.a₁ * x + W.a₃ = 1 ^ 3 * (W.a₃ + x * W.a₁ + 2 * y)

Tactic:
ring1

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

Goal state before:
pp: case e'_2
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) =
    1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * x ^ 2 - 2 * 0 * y)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
hΔ : W.a₆ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0
⊢ -(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 * (W.a₁ ^ 2 * 0 + 4 * W.a₂ * 0 - W.a₁ * 0 * 0 + W.a₂ * 0 ^ 2 - 0 ^ 2) -
          8 * (2 * 0 + W.a₁ * 0) ^ 3 -
        27 * (0 ^ 2 + 4 * 0) ^ 2 +
      9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * 0 + W.a₁ * 0) * (0 ^ 2 + 4 * 0) =
    0

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (2 * Y + (C (C W'.a₁) * C X + C (C W'.a₃))) = -Y - (C (C W'.a₁) * C X + C (C W'.a₃))

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(-y - W'.a₁ * x - W'.a₃) - W'.a₁ * x - W'.a₃ = y

Tactic:
ring1

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

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

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

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x (W'.negY x y) ↔ W'.Equation x y

Tactic:
rw [equation_iff, equation_iff, negY]
  congr! 1
  ring1

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

Goal state before:
pp: case e_a
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₂
⊢ y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) = 2 * y₁ + W.a₁ * x₁ + W.a₃

Tactic:
ring1

Goal state after:
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t

Tactic:
have := Scheme.compactSpace_of_isLimit _ _ hc

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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

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

Tactic:
ring1

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

Goal state before:
pp: case right
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✝
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k✝ * (1 + Multiset.count 0 d)
B : Multiset (Fin n) := Finsupp.toMultiset (Finsupp.comapDomain Fin.succ (Multiset.toFinsupp d) ⋯)
k : ℕ
C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hxS : C ∈ S
j : Fin { f := (MvPolynomial.finSuccEquiv R n) C.f, n := C.n, g := ⇑(MvPolynomial.finSuccEquiv R n) ∘ C.g }.n
hS : ∀ (a : Fin (n + 1)), degreeOf a (C.g j) ≤ Multiset.count a d
a : Fin n
⊢ degreeOf a (((MvPolynomial.finSuccEquiv R n) (C.g j)).coeff k) ≤ Multiset.count a.succ d

Tactic:
exact (degreeOf_coeff_finSuccEquiv (C.g j) a k).trans (hS _)

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

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

Tactic:
ring1

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

Goal state before:
pp: case a₁
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 * (W.a₁ + 2 * 0) = W.a₁

Tactic:
ring1

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

Goal state before:
pp: case a₂
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 2 * (W.a₂ - 0 * W.a₁ + 3 * 0 - 0 ^ 2) = W.a₂

Tactic:
ring1

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

Goal state before:
pp: case a₃
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 3 * (W.a₃ + 0 * W.a₁ + 2 * 0) = W.a₃

Tactic:
ring1

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

Goal state before:
pp: case a₄
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * 0 * W.a₂ - (0 + 0 * 0) * W.a₁ + 3 * 0 ^ 2 - 2 * 0 * 0) = W.a₄

Tactic:
ring1

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

Goal state before:
pp: case a₆
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 6 * (W.a₆ + 0 * W.a₄ + 0 ^ 2 * W.a₂ + 0 ^ 3 - 0 * W.a₃ - 0 ^ 2 - 0 * 0 * W.a₁) = W.a₆

Tactic:
ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) =
    ↑C.u⁻¹ ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂ + 12 * C.r)

Tactic:
ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 2 * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
      ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) =
    ↑C.u⁻¹ ^ 4 * (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (W.a₁ ^ 2 + 4 * W.a₂) + 6 * C.r ^ 2)

Tactic:
ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 +
      4 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) =
    ↑C.u⁻¹ ^ 6 *
      (W.a₃ ^ 2 + 4 * W.a₆ + 2 * C.r * (2 * W.a₄ + W.a₁ * W.a₃) + C.r ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂) + 4 * C.r ^ 3)

Tactic:
ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 *
              (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) +
            4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) *
              (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) -
          ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) *
            (↑C.u⁻¹ ^ 4 *
              (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
        ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 -
      (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) ^ 2 =
    ↑C.u⁻¹ ^ 8 *
      (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 +
              3 * C.r * (W.a₃ ^ 2 + 4 * W.a₆) +
            3 * C.r ^ 2 * (2 * W.a₄ + W.a₁ * W.a₃) +
          C.r ^ 3 * (W.a₁ ^ 2 + 4 * W.a₂) +
        3 * C.r ^ 4)

Tactic:
ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 2 - 24 * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) =
    ↑C.u⁻¹ ^ 4 * (W.b₂ ^ 2 - 24 * W.b₄)

Tactic:
ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ -(↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 3 +
        36 * (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) -
      216 * (↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)) =
    ↑C.u⁻¹ ^ 6 * (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)

Tactic:
ring1

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

Goal state before:
pp: case pos.b
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ -((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 -
        W.a₁ * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
      W.a₂ =
    -(x₁ + x₁ +
        (((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 +
                W.a₁ * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
              W.a₂ -
            x₁ -
          x₁))

Tactic:
ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ -((↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2))) ^ 2 *
            ((↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 *
                      (↑C.u⁻¹ ^ 6 *
                        (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) +
                    4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) *
                      (↑C.u⁻¹ ^ 6 *
                        (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) -
                  ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) *
                    (↑C.u⁻¹ ^ 4 *
                      (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
                ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2) *
                  (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 -
              (↑C.u⁻¹ ^ 4 *
                  (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) ^
                2) -
          8 *
            (2 *
                  (↑C.u⁻¹ ^ 4 *
                    (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
                ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t))) ^
              3 -
        27 *
          ((↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 +
              4 *
                (↑C.u⁻¹ ^ 6 *
                  (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁))) ^
            2 +
      9 * ((↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2))) *
          (2 *
              (↑C.u⁻¹ ^ 4 *
                (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
            ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t))) *
        ((↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 +
          4 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁))) =
    ↑C.u⁻¹ ^ 12 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆))

Tactic:
ring1

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

Goal state before:
pp: case pos.c
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
        (x₁ * 2 * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) +
          (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (x₁ * W.a₁ - 2 * y₁ - W.a₃)) +
      (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (-(W.a₁ * y₁) + W.a₄) =
    x₁ *
      ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
              (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
            W.a₂ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
          x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 +
        ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
              W.a₂ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
            x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
          x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2))

Tactic:
ring1

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

Goal state before:
pp: case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
            (-(x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁)) +
              (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (2 * y₁ + W.a₃)) -
          (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (y₁ * (y₁ + W.a₃) - W.a₆) +
        y₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (y₁ + x₁ * W.a₁ + W.a₃) -
      (-(x₁ ^ 2 *
            ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                    (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
                  W.a₂ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
                x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
              x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2)) +
        (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (x₁ * (x₁ * (x₁ + W.a₂) + W.a₄) + W.a₆)) =
    0

Tactic:
ring1

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)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k * (1 + Multiset.count 0 d)
B : Multiset (Fin n) := Finsupp.toMultiset (Finsupp.comapDomain Fin.succ (Multiset.toFinsupp d) ⋯)
T : ConstructibleSetData (MvPolynomial (Fin n) R)
hT₁ : comap Polynomial.C '' S'.toSet = T.toSet
hT₂ :
  ∀ C ∈ T,
    C.n ≤ S'.degBound ∧
      ∀ (i : Fin C.n),
        C.g i ∈ (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) ^ S'.degBound ^ S'.degBound
N : ℕ := (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d))
this :
  ∀ C ∈ T, ∀ (a : Fin C.n), C.g a ∈ coeffsIn (Fin n) (M ^ N) ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))
h1M : 1 ≤ M
U : ConstructibleSetData R
hU₁ : comap MvPolynomial.C '' T.toSet = U.toSet
hU₂ :
  ∀ C ∈ U,
    C.n ≤
        numBound S'.degBound
          (fun i ↦
            1 +
              (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                Multiset.count i (Multiset.map Fin.val B))
          n ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          M ^
            ((k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
              degBound S'.degBound
                (fun i ↦
                  1 +
                    (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                      Multiset.count i (Multiset.map Fin.val B))
                n)
t : ℕ
ht✝ : t + 1 < n + 1
ht : t < n
⊢ 1 + Multiset.count ⟨t, ht⟩ B ≤ 1 + Multiset.count ⟨t + 1, ht✝⟩ d

Tactic:
simp [B]

Goal state after: