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

Goal state before:
pp: n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector f v))) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i) = v i

Tactic:
← toSpecMvPolyIntEquiv_comp,

Goal state after:
n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (toSpecMvPolyIntEquiv n) (homOfVector f v ≫ toSpecMvPoly n S) i = v i
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite

Tactic:
intro z hz
      obtain ⟨t₁, ht₁⟩ := hf.2 z hz
      obtain ⟨t₂, ht₂⟩ := hg.2 z hz
      use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
      apply Set.Finite.subset (s := (t₁ ∩ f.support) ∪ (t₂ ∩ g.support)) (ht₁.2.union ht₂.2)
      intro a ha
      simp_all only [support_subset_iff, ne_eq, mem_ofPred_eq,
        mem_inter_iff, mem_support, Pi.add_apply, mem_union, true_and]
      by_contra! hCon
      simp_all

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support fun i ↦ ⇑(F i)
h : ¬(Function.support F).Finite
⊢ ⇑(∑ᶠ (i : ι), F i) = ∑ᶠ (i : ι), ⇑(F i)

Tactic:
· simp_all [finsum_of_infinite_support]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ (D⁻.restrict h) x = (D.restrict h)⁻ x

Tactic:
simp only [locallyFinsuppWithin.restrict_apply, locallyFinsuppWithin.negPart_apply]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ (if x ∈ V then (D x)⁻ else 0) = (if x ∈ V then D x else 0)⁻
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
⊢ φRX ≫ X.presheaf.map ⋯.hom.op =
    φRA ≫
      CommRingCat.ofHom
        (e.symm.toRingHom.comp
          ((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯))

Tactic:
· ext a
    apply e.injective
    change e _ = e (e.symm _)
    rw [RingEquiv.apply_symm_apply]
    ext
    change X.presheaf.germ _ _ _ (X.presheaf.map _ _) = (φRA ≫ φ) a
    rw [TopCat.Presheaf.germ_res_apply, ‹φRA ≫ φ = _›]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ X.homOfLE ⋯ ≫
      Cover.glueMorphisms f.toRationalMap.openCoverDomain (fun x ↦ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom) ⋯ =
    f.hom

Tactic:
refine (f.toRationalMap.openCoverDomain.ι_glueMorphisms _ _ ⟨_, f, rfl, rfl⟩).trans ?_

Goal state after:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom = f.hom
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✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
x✝¹ : ∀ (i : I), Nonempty ↥(D'.obj i)
x✝ : ∀ (i : I), CompactSpace ↥(D'.obj i)
c' : Cone D' :=
  { pt := (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subscheme,
    π :=
      {
        app := fun i ↦
          (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeMap
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
⊢ Scheme.Hom.ker (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeι ≤
    Scheme.Hom.ker (hc.lift ((Cone.postcompose ι).obj s))

Tactic:
by
      suffices ∀ i, vanishingIdeal ⟨Z i, hZc i⟩ ≤ (s.π.app i ≫ ι.app i).ker by
        simpa [← le_map_iff_comap_le, ← Scheme.Hom.ker_comp]
      refine fun i ↦ .trans ?_ (Scheme.Hom.le_ker_comp _ _)
      simp [ι]

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j : (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).I₀
⊢ (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).f j ≫ W ↘ S = (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).X j ↘ S

Tactic:
by exact (pullback.fst (f.asOverProp S) ((𝒰.f j).asOverProp S)).w

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: case refine_2.refine_1
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ cospan f f ⋙ F ≅ cospan (F.map f) (F.map f)

Tactic:
exact cospanIsoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Goal state after:
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
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶ ↑↑(↑i).2 := IsOpenImmersion.lift (Opens.ι ↑(↑i).2) (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ fst π π
h2 :
  snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ snd π π
⊢ fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ f' = snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ f'

Tactic:
by
    simp only [← cancel_mono (Scheme.Opens.ι i.1.2.1),
      Category.assoc, IsOpenImmersion.lift_fac, f', reassoc_of% h1, reassoc_of% h2, hf]

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

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

Tactic:
by
  rw [b₈]
  linear_combination W.a₂ * W.a₆ * CharP.cast_eq_zero R 3

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.twoTorsionPolynomial.discr = 0

Tactic:
linear_combination W.twoTorsionPolynomial_discr + 8 * W.Δ * CharP.cast_eq_zero R 2

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

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ degBound k₀ (fun t ↦ Nat.casesOn t k D) (n + 1 + 1) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
rw [degBound_succ, numBound_casesOn_succ, degBound_casesOn_succ, numBound_succ, degBound_succ,
      numBound_succ]

Goal state after:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) ^
        (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) *
      ((numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) ^
          (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) *
        degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case zero.refine_2
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ ∀ C ∈ ConstructibleSetData.map (isEmptyRingEquiv R (Fin 0)).toRingHom S,
    C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0 ∧
      ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0

Tactic:
simp only [ConstructibleSetData.map, RingEquiv.toRingHom_eq_coe, Finset.mem_image, comp_apply,
        BasicConstructibleSetData.map, RingHom.coe_coe, isEmptyRingEquiv_eq_coeff_zero, pow_one,
        numBound_zero, degBound_zero, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Goal state after:
case zero.refine_2
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ ∀ a ∈ S, a.n ≤ k ∧ ∀ (i : Fin a.n), MvPolynomial.coeff 0 (a.g i) ∈ M
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (C * C') • W = C • C' • W

Tactic:
simp only [VariableChange.mul_def, variableChange_def]

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

Tactic:
sub_eq_zero

Goal state after:
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₆ ↔
    y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
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
hgj : ¬C.g j = 0
⊢ ((MvPolynomial.finSuccEquiv R n) (C.g j)).degree.succ ≤ 1 + Multiset.count 0 d

Tactic:
degree_finSuccEquiv hgj,

Goal state after:
case neg
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
hgj : ¬C.g j = 0
⊢ (↑(degreeOf 0 (C.g j))).succ ≤ 1 + Multiset.count 0 d
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - W'.negPolynomial = W'.polynomialY

Tactic:
by
  rw [← Y_sub_polynomialY, sub_sub_cancel]

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

Goal state before:
pp: case left
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] := ⋯
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ⋯
hS' : S'.degBound ≤ k✝ * (1 + Multiset.count 0 d)
B : Multiset (Fin n) := ⋯
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
⊢ ∀ (i : Fin n →₀ ℕ), MvPolynomial.coeff i (((MvPolynomial.finSuccEquiv R n) (C.g j)).coeff k) ∈ M

Tactic:
intro d
          simp only [finSuccEquiv_coeff_coeff]
          exact (hS _ hxS _).1 _

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
⊢ finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree

Tactic:
by
  have := Fintype.ofFinite ι
  have h := span_singleton_eq_bot.not.2 hf
  rw [natDegree_eq_of_degree_eq
      (degree_eq_degree_of_associated <| associated_norm_prod_smith b hf)]
  rw [natDegree_prod _ _ fun i _ => smithCoeffs_ne_zero b _ h i, finrank_quotient_eq_sum F h b]
  congr with i
  exact (AdjoinRoot.powerBasis <| smithCoeffs_ne_zero b _ h i).finrank

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 {(mk W) (C (X - C x))} *
      (span {(mk W) (C (X - C x))} ⊔
        (span {(mk W) (Y - C (C y))} ⊔
          (span {(mk W) (Y - C (C (W.negY x y)))} ⊔
            span
              {(AdjoinRoot.mk W.polynomial)
                  (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)}))) =
    XIdeal W x

Tactic:
← span_insert

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))} *
      span
        {(mk W) (C (X - C x)), (mk W) (Y - C (C y)), (mk W) (Y - C (C (W.negY x y))),
          (AdjoinRoot.mk W.polynomial) (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)} =
    XIdeal W x
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
⊢ Ideal.map (mk W)
      (span
        {C (X - C x), Y - C (C y), Y - C (C (W.negY x y)),
          C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y}) =
    Ideal.map (mk W) ⊤

Tactic:
apply congr_arg

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
      {C (X - C x), Y - C (C y), Y - C (C (W.negY x y)),
        C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y} =
    ⊤
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case inl
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
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))

Tactic:
let W_X := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
    refine
      ⟨C <| C W_X⁻¹ * -(X + C (2 * x + W.a₂)), C <| C <| W_X⁻¹ * W.a₁, 0, C <| C <| W_X⁻¹ * -1, ?_⟩
    rw [← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hx]
    simp only [W_X, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hx]
    C_simp
    ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b : ℤ
⊢ atom W |a| b = atom W a b

Tactic:
by
  rcases abs_choice a with h | h <;> simp only [h, atom_neg_left odd]

Goal state after: