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

Goal state before:
pp: 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_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ ((pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (Cover.trans 𝒰 hij ≫ 𝒰.f j) (𝟙 (D.obj a).left) (𝟙 (𝒰.X i)) (𝟙 S) ⋯
            ⋯ ≫
          (pullbackLeftPullbackSndIso (D.obj a).hom (𝒰.f j) (Cover.trans 𝒰 hij)).inv) ≫
        𝟙 (pullback (pullback.snd (D.obj a).hom (𝒰.f j)) (Cover.trans 𝒰 hij))) ≫
      pullback.fst (pullback.snd (D.obj a).hom (𝒰.f j)) (Cover.trans 𝒰 hij) ≫
        (Comma.Hom.hom ((d.cocone j).ι.app a)).left =
    pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (𝒰.f j) (𝟙 (D.obj a).left) (Cover.trans 𝒰 hij) (𝟙 S) ⋯ ⋯ ≫
      (Comma.Hom.hom ((d.cocone j).ι.app a)).left

Tactic:
Category.comp_id,

Goal state after:
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_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ (pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (Cover.trans 𝒰 hij ≫ 𝒰.f j) (𝟙 (D.obj a).left) (𝟙 (𝒰.X i)) (𝟙 S) ⋯
          ⋯ ≫
        (pullbackLeftPullbackSndIso (D.obj a).hom (𝒰.f j) (Cover.trans 𝒰 hij)).inv) ≫
      pullback.fst (pullback.snd (D.obj a).hom (𝒰.f j)) (Cover.trans 𝒰 hij) ≫
        (Comma.Hom.hom ((d.cocone j).ι.app a)).left =
    pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (𝒰.f j) (𝟙 (D.obj a).left) (Cover.trans 𝒰 hij) (𝟙 S) ⋯ ⋯ ≫
      (Comma.Hom.hom ((d.cocone j).ι.app a)).left
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case e'_6
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : IsEmpty ↥S
U : S.Opens
hU : IsAffineOpen U
⊢ ↑U = ∅

Tactic:
simp [eq_bot_iff]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
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.266} 𝒰.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.266} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
this : (𝒱 a).f i ≫ (D.map f).left = ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f).left ≫ (𝒱 b).f i
⊢ (𝒱 a).f i ≫
      (Comma.Hom.hom (D.map f)).left ≫
        ((𝒱 b).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯).left =
    (𝒱 a).f i ≫
      ((𝒱 a).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯).left ≫
        𝟙 d.glued.left

Tactic:
Category.comp_id,

Goal state after:
case refine_2
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.266} 𝒰.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.266} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
this : (𝒱 a).f i ≫ (D.map f).left = ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f).left ≫ (𝒱 b).f i
⊢ (𝒱 a).f i ≫
      (Comma.Hom.hom (D.map f)).left ≫
        ((𝒱 b).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯).left =
    (𝒱 a).f i ≫
      ((𝒱 a).glueMorphismsOverOfLocallyDirected
          (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯).left
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑{ u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
          r :=
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r *
                ↑C.u ^ 2 +
              C.r,
          s :=
            ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
              C.s,
          t :=
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t *
                  ↑C.u ^ 3 +
                { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r *
                    C.s *
                  ↑C.u ^ 2 +
              C.t }.u =
    ↑{ u := 1, r := 0, s := 0, t := 0 }.u

Tactic:
dsimp only

Goal state after:
case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑(C.u⁻¹ * C.u) = ↑1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.r =
    { u := 1, r := 0, s := 0, t := 0 }.r

Tactic:
dsimp only

Goal state after:
case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ -C.r * ↑C.u⁻¹ ^ 2 * ↑C.u ^ 2 + C.r = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.s =
    { u := 1, r := 0, s := 0, t := 0 }.s

Tactic:
dsimp only

Goal state after:
case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
            C.r,
        s :=
          ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
              { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
                ↑C.u ^ 2 +
            C.t }.t =
    { u := 1, r := 0, s := 0, t := 0 }.t

Tactic:
dsimp only

Goal state after:
case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 * ↑C.u ^ 3 + -C.r * ↑C.u⁻¹ ^ 2 * C.s * ↑C.u ^ 2 + C.t = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial ≠ 0

Tactic:
rw [polynomial_eq]
  exact Cubic.ne_zero_of_b_ne_zero one_ne_zero

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

Goal state before:
pp: 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) ⋯)
⊢ 1 ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)

Tactic:
by simpa [MvPolynomial.coeff_one, apply_ite] using hM

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
⊢ { a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s),
        a₂ :=
          1 ^ 2 *
            (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r -
              { u := 1, r := 0, s := 0, t := 0 }.s ^ 2),
        a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₄ :=
          1 ^ 4 *
            (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ -
                  ({ u := 1, r := 0, s := 0, t := 0 }.t +
                      { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) *
                    W.a₁ +
                3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 -
              2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₆ :=
          1 ^ 6 *
            (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ +
                    { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 -
                  { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ -
                { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 -
              { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) }.a₁ =
    W.a₁

Tactic:
dsimp only

Goal state after:
case a₁
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 * (W.a₁ + 2 * 0) = W.a₁
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
⊢ { a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s),
        a₂ :=
          1 ^ 2 *
            (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r -
              { u := 1, r := 0, s := 0, t := 0 }.s ^ 2),
        a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₄ :=
          1 ^ 4 *
            (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ -
                  ({ u := 1, r := 0, s := 0, t := 0 }.t +
                      { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) *
                    W.a₁ +
                3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 -
              2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₆ :=
          1 ^ 6 *
            (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ +
                    { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 -
                  { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ -
                { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 -
              { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) }.a₂ =
    W.a₂

Tactic:
dsimp only

Goal state after:
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₂
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
⊢ { a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s),
        a₂ :=
          1 ^ 2 *
            (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r -
              { u := 1, r := 0, s := 0, t := 0 }.s ^ 2),
        a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₄ :=
          1 ^ 4 *
            (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ -
                  ({ u := 1, r := 0, s := 0, t := 0 }.t +
                      { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) *
                    W.a₁ +
                3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 -
              2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₆ :=
          1 ^ 6 *
            (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ +
                    { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 -
                  { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ -
                { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 -
              { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) }.a₃ =
    W.a₃

Tactic:
dsimp only

Goal state after:
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₃
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
⊢ { a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s),
        a₂ :=
          1 ^ 2 *
            (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r -
              { u := 1, r := 0, s := 0, t := 0 }.s ^ 2),
        a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₄ :=
          1 ^ 4 *
            (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ -
                  ({ u := 1, r := 0, s := 0, t := 0 }.t +
                      { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) *
                    W.a₁ +
                3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 -
              2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₆ :=
          1 ^ 6 *
            (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ +
                    { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 -
                  { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ -
                { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 -
              { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) }.a₄ =
    W.a₄

Tactic:
dsimp only

Goal state after:
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₄
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
⊢ { a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s),
        a₂ :=
          1 ^ 2 *
            (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r -
              { u := 1, r := 0, s := 0, t := 0 }.s ^ 2),
        a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₄ :=
          1 ^ 4 *
            (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ -
                  ({ u := 1, r := 0, s := 0, t := 0 }.t +
                      { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) *
                    W.a₁ +
                3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 -
              2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₆ :=
          1 ^ 6 *
            (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ +
                    { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 -
                  { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ -
                { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 -
              { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) }.a₆ =
    W.a₆

Tactic:
dsimp only

Goal state after:
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₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

Tactic:
simp only [b₂, variableChange_a₁, variableChange_a₂]

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
n : Fin 2
a✝ : Nontrivial R
⊢ (CoordinateRing.basis W') n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Tactic:
rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
    PowerBasis.basis_eq_pow, finCongr_symm_apply, Fin.val_cast]

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

Goal state before:
pp: case pos
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₂)
hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : ¬n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n

Tactic:
· simp [complEDS, Int.sign_natCast_of_ne_zero hn]

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

Goal state before:
pp: case neg.some
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.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hp' : p.degree = some 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 • q.degree + 3)

Tactic:
hp'

Goal state after:
case neg.some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some 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 • q.degree + 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Tactic:
rw [b₈, a₁_of_isCharNeTwoNF, a₃_of_isCharNeTwoNF]
  ring1

Goal state after: