mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : ¬-f x < 0
⊢ max (-(n • f x)) 0 = n • max (-f x) 0

Tactic:
· simpa [not_lt.1 h] using nsmul_nonneg (not_lt.1 h) n

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
⊢ ∃ z, D z ≠ 0

Tactic:
simpa [D.ext_iff] using! (ne_of_lt h).symm

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx : ¬(if x ∈ V then D x else 0) = 0
⊢ x ∈ V

Tactic:
ite_eq_right_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx : ¬(x ∈ V → D x = 0)
⊢ x ∈ V
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
f : locallyFinsuppWithin U Y
p : X
hp : p ∈ U
t : Set X
h₁t : t ∈ 𝓝 p
h₂t : (t ∩ f.support).Finite
⊢ t ∩ f.support ∈ 𝓝[f.support] p

Tactic:
rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
f : locallyFinsuppWithin U Y
p : X
hp : p ∈ U
t : Set X
h₁t : t ∈ 𝓝 p
h₂t : (t ∩ f.support).Finite
⊢ ∃ u ∈ 𝓝 p, u ∩ f.support ⊆ t ∩ f.support
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
V : Y.Opens
hV : Dense ↑V
hV' : V ≤ g.domain
⊢ (f.comp (g.restrict V hV hV')).hom = (X.isoOfEq ⋯).hom ≫ ((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ V) ⋯ ⋯).hom

Tactic:
simp [← f.domain.ι.isoImage_inv_homOfLE_assoc _ _ (f.hom.preimage_mono hV'),
      ← morphismRestrict_homOfLE_assoc f.hom _ _ hV']

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

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)

Tactic:
rw [← f₃.toRationalMap_representative]
  simp_rw [comp_def, ← PartialMap.comp_assoc, PartialMap.toRationalMap_eq_iff]
  apply PartialMap.comp_equiv_of_equiv_left
  rw [← f₂.toRationalMap_representative, comp_def]
  apply (f₁.representative.comp f₂.representative).representative_toRationalMap_equiv.trans
  apply PartialMap.comp_equiv_of_equiv_right
  rw [toRationalMap_representative]

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

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝³ : Category.{v_1, ?u.118} 𝒰.I₀
inst✝² : 𝒰.LocallyDirected
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
i j : 𝒰.I₀
k :
  { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j), X := fun k ↦ 𝒰.X k.fst,
      f := fun k ↦ pullback.lift (𝒰.trans k.snd.1) (𝒰.trans k.snd.2) ⋯ }.I₀
⊢ P (𝒰.trans k.snd.1)

Tactic:
exact 𝒰.property_trans _

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

Goal state before:
pp: X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (PartialMap.id X).comp f = f

Tactic:
by
  ext1
  · simp_rw [comp_domain, Hom.toPartialMap_domain, Hom.toPartialMap_hom, Category.comp_id,
      ← X.topIso_hom, ← Hom.inv_image, ← Hom.comp_image, Iso.inv_hom_id, Hom.id_image]
  · simp_rw [comp_hom, Hom.toPartialMap_hom, Hom.toPartialMap_domain, morphismRestrict_comp,
      morphismRestrict_id, ← X.topIso_hom, Hom.comp_preimage, Hom.id_preimage,
      Category.comp_id, ← X.topIso.hom.isoImage_preimage_hom_homOfLE, Category.assoc,
      Iso.inv_hom_id_assoc]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↥(pullback.diagonalObj f)
⊢ (pullback.fst f f) ((pullback.diagonal f) ((pullback.fst f f) x)) = (pullback.fst f f) x

Tactic:
rw [← Scheme.Hom.comp_apply, pullback.diagonal_fst]

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↥(pullback.diagonalObj f)
⊢ (𝟙 X) ((pullback.fst f f) x) = (pullback.fst f f) x
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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : (c.π.app i) x ∈ ↑V
this✝ : ∀ (j : (Over i)ᵒᵖ), IsAffine (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine ((opensDiagram D i V).obj j)
r : ↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
hrU : (((Functor.const I).obj c.pt).obj i).basicOpen r ≤ U
hxr : ↑⟨x, hxU⟩ ∈ (((Functor.const I).obj c.pt).obj i).basicOpen r
j : Over i
s : ↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V)
hs :
  (ConcreteCategory.hom (((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).ι.app (Opposite.op j)))
      ((D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv s) =
    (ConcreteCategory.hom (c.π.app i ⁻¹ᵁ V).topIso.inv) r
⊢ ∃ U' ∈ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}, x ∈ U' ∧ U' ≤ U

Tactic:
have h : c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ V := congr($(c.w j.hom) ⁻¹ᵁ V)

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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : (c.π.app i) x ∈ ↑V
this✝ : ∀ (j : (Over i)ᵒᵖ), IsAffine (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine ((opensDiagram D i V).obj j)
r : ↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
hrU : (((Functor.const I).obj c.pt).obj i).basicOpen r ≤ U
hxr : ↑⟨x, hxU⟩ ∈ (((Functor.const I).obj c.pt).obj i).basicOpen r
j : Over i
s : ↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V)
hs :
  (ConcreteCategory.hom (((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).ι.app (Opposite.op j)))
      ((D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv s) =
    (ConcreteCategory.hom (c.π.app i ⁻¹ᵁ V).topIso.inv) r
h : c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ V
⊢ ∃ U' ∈ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}, x ∈ U' ∧ U' ≤ U
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)
⊢ CompactSpace ↥c.pt

Tactic:
by
  obtain ⟨i⟩ := IsCofiltered.nonempty (C := I)
  have := isAffineHom_π_app _ _ hc
  exact QuasiCompact.compactSpace_of_compactSpace (c.π.app i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case h
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
x : ↥s.pt
⊢ (𝒰.f i) (s.fst x) = d.toBase (s.snd x)

Tactic:
rw [← Scheme.Hom.comp_apply, ← s.condition]

Goal state after:
case h
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
x : ↥s.pt
⊢ (𝒰.f i) (s.fst x) = (s.fst ≫ 𝒰.f i) x
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
⊢ QuasiCompactCover (PreZeroHypercover.pullback₁ f 𝒰)

Tactic:
refine ⟨fun {U'} hU' ↦ ?_⟩

Goal state after:
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
⊢ IsCompactOpenCovered (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) ↑U'
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ EffectiveEpi f.base

Tactic:
rw [TopCat.effectiveEpi_iff_isQuotientMap]
  exact Flat.isQuotientMap_of_surjective _

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.442} 𝒰.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.442} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
⊢ ∀ (s : Cocone D) (m : d.gluedCocone.pt ⟶ s.pt),
    (∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j) →
      m =
        {
          toCommaMorphism :=
            𝒱.glueMorphismsOverOfLocallyDirected
              (fun i ↦
                ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                  pullback.fst s.pt.hom (𝒰.f i))
              ⋯ ⋯,
          prop_hom_left := trivial, prop_hom_right := trivial }

Tactic:
intro s m hm

Goal state after:
case refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.442} 𝒰.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.442} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
⊢ m =
    {
      toCommaMorphism :=
        𝒱.glueMorphismsOverOfLocallyDirected
          (fun i ↦
            ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
              pullback.fst s.pt.hom (𝒰.f i))
          ⋯ ⋯,
      prop_hom_left := trivial, prop_hom_right := trivial }
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).b₆ = f W.b₆

Tactic:
simp only [b₆, map_a₃, map_a₆]

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ f W.a₃ ^ 2 + 4 * f W.a₆ = f (W.a₃ ^ 2 + 4 * W.a₆)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 • W = W

Tactic:
rw [VariableChange.one_def, variableChange_def, inv_one, Units.val_one]
    ext <;> dsimp only <;> 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
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ map 1 φ = 1

Tactic:
simp only [one_def, map]
    ext <;> simp only [map_one, Units.val_one, map_zero]

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

Goal state before:
pp: case succ.refine_2
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)
this :
  ∀ i < n + 1,
    (Nat.casesOn i (1 + Multiset.count 0 d) fun x ↦ 1 + Multiset.count x (Multiset.map Fin.val B)) ≤
      1 + Multiset.count i (Multiset.map Fin.val d)
C : BasicConstructibleSetData R
hCU : C ∈ U
x✝¹ : ℕ
x✝ : x✝¹ < n
⊢ 1 + (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) * Multiset.count x✝¹ (Multiset.map Fin.val B) ≤
    ((k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) • fun x ↦
        1 + Multiset.count x (Multiset.map Fin.val B))
      x✝¹

Tactic:
simp +contextual [mul_add, Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: case succ.refine_3
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)
this :
  ∀ i < n + 1,
    (Nat.casesOn i (1 + Multiset.count 0 d) fun x ↦ 1 + Multiset.count x (Multiset.map Fin.val B)) ≤
      1 + Multiset.count i (Multiset.map Fin.val d)
C : BasicConstructibleSetData R
hCU : C ∈ U
i : Fin C.n
x✝¹ : ℕ
x✝ : x✝¹ < n
⊢ 1 + (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) * Multiset.count x✝¹ (Multiset.map Fin.val B) ≤
    ((k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) • fun x ↦
        1 + Multiset.count x (Multiset.map Fin.val B))
      x✝¹

Tactic:
simp +contextual [mul_add, Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (W.map f).slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_Y_ne (congr_arg f hx) <| map_negY f x₂ y₂ ▸ fun h => hy <| f.injective h,
        map_negY, slope_of_Y_ne hx hy]
      map_simp

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

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (W.map f).slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
· rw [slope_of_Y_ne (congr_arg f hx) <| map_negY f x₂ y₂ ▸ fun h => hy <| f.injective h,
        map_negY, slope_of_Y_ne hx hy]
      map_simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3.refine_2
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)
k : 𝒰.I₀
s : PullbackCone ⋯.fromSpec (c.π.app i)
y : ↥s.pt
⊢ (c.π.app i) (s.snd y) ∈ V k

Tactic:
rw [← Scheme.Hom.comp_apply, ← s.condition]

Goal state after:
case refine_3.refine_2
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)
k : 𝒰.I₀
s : PullbackCone ⋯.fromSpec (c.π.app i)
y : ↥s.pt
⊢ (s.fst ≫ ⋯.fromSpec) y ∈ V k
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3
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)
⊢ ∀ (j : 𝒰.I₀),
    IsPullback ((fun k ↦ IsOpenImmersion.lift (V k).ι (𝒰.f k ≫ c.π.app i) ⋯ ≫ ⋯.isoSpec.hom) j) (𝒰.f j)
      ((fun k ↦ ⋯.isoSpec.inv ≫ (V k).ι) j) (c.π.app i)

Tactic:
· intro k
    dsimp
    refine ⟨⟨?_⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
    · simp [← IsAffineOpen.isoSpec_inv_ι]
    · intro s
      refine IsOpenImmersion.lift (𝒰.f k) s.snd ?_
      simp only [hV'', Set.range_subset_iff, Set.mem_preimage, SetLike.mem_coe]
      intro y
      rw [← Scheme.Hom.comp_apply, ← s.condition]
      simp [← IsAffineOpen.isoSpec_inv_ι]
    · simp [← cancel_mono (hV' _).left.isoSpec.inv, ← cancel_mono (V k).ι, PullbackCone.condition]
    · simp
    · simp [← cancel_mono (𝒰.f k)]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
P Q : W.Point
⊢ P.xRep = Q.xRep ↔ P = Q ∨ P = -Q

Tactic:
refine ⟨eq_or_eq_neg_of_xRep_eq_xRep, fun H ↦ ?_⟩
  rcases H with rfl | rfl <;> simp

Goal state after:
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
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).preΨ n = Polynomial.map (↑f) ((W⁄A).preΨ n)

Tactic:
by
  rw [← map_preΨ, map_baseChange]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n)

Tactic:
let dm {m n p q} : _ → _ → (p * q : R[X]).natDegree ≤ m + n := natDegree_mul_le_of_le

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
⊢ (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1

Tactic:
let dm {m n p q} : _ → _ → (p * q : R[X]).natDegree ≤ m + n := natDegree_mul_le_of_le

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
⊢ (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1