mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ ((algebraMap S (Localization.Away (f t))).comp (algebraMap R S))
      ((algebraMap S (Localization.Away (f t))) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩) *
        (algebraMap S (Localization.Away (f t))) r)
      p =
    0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
← map_mul,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ ((algebraMap S (Localization.Away (f t))).comp (algebraMap R S))
      ((algebraMap S (Localization.Away (f t))) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r)) p =
    0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: Z S : Scheme
⊢ @IsIntegralHom ≤ topologically @IsClosedMap

Tactic:
intro X

Goal state after:
Z S X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), IsIntegralHom f → topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
⊢ IsIntegralHom f

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hX : ∃ S, X = Spec S
⊢ IsIntegralHom f
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := ⋯
i : 𝒰.I₀
⊢ IsOpen (⇑(𝒰.f i) ⁻¹' s)

Tactic:
refine this (f := pullback.fst (𝒰.f i) f) _ ?_ ⟨_, rfl⟩

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(pullback.fst (𝒰.f i) f) ⁻¹' ⇑(𝒰.f i) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
⊢ IsOpen s

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
⊢ IsOpen s

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
hX : ∃ S, X = Spec S
⊢ IsOpen s
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
Y : Type u_2
inst✝² : DecidableEq X
inst✝¹ : Zero Y
inst✝ : Preorder Y
x : X
y : Y
⊢ ⇑0 < ⇑(single x y) ↔ 0 < y

Tactic:
coe_single

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
Y : Type u_2
inst✝² : DecidableEq X
inst✝¹ : Zero Y
inst✝ : Preorder Y
x : X
y : Y
⊢ ⇑0 < Pi.single x y ↔ 0 < y
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: 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
⊢ (n • f)⁺ = n • f⁺

Tactic:
ext x
  simp only [posPart, max_apply, coe_nsmul, Pi.smul_apply, coe_zero, Pi.zero_apply]
  by_cases h : f x < 0
  · simpa [max_eq_right_of_lt h] using nsmul_le_nsmul_right h.le n
  · simpa [not_lt.1 h] using nsmul_nonneg (not_lt.1 h) n

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

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
⊢ f = g ↔ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
by
  constructor
  · rintro rfl
    simp
  · obtain ⟨U, hU, f⟩ := f
    obtain ⟨V, hV, g⟩ := g
    rintro ⟨rfl : U = V, e⟩
    congr 1
    simpa using e

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
⊢ ∀ ⦃a b : X.PartialMap Y⦄, a ≈ b → a.compHom g ≈ b.compHom g

Tactic:
intro f₁

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ : X.PartialMap Y
⊢ ∀ ⦃b : X.PartialMap Y⦄, f₁ ≈ b → f₁.compHom g ≈ b.compHom g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
⊢ Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom =
    Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom

Tactic:
have hg₂ (x) : (g x).domain = x.1 := x.2.choose_spec.2

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom =
    Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom
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 ⟶ Z
⊢ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ ⊤)).inv ≫ (f.hom ⁻¹ᵁ ⊤).ι ≫ f.hom ≫ g = (X.isoOfEq ⋯).hom ≫ f.hom ≫ g

Tactic:
f.domain.isoImage_ι_inv_ι_assoc,

Goal state after:
case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ X.homOfLE ⋯ ≫ f.hom ≫ g = (X.isoOfEq ⋯).hom ≫ f.hom ≫ g
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X ⤏ Y
inst✝¹ : f.IsDominant
g : Y ⤏ Z
inst✝ : g.IsDominant
⊢ (f.comp g).IsDominant

Tactic:
← g.toRationalMap_representative,

Goal state after:
X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X ⤏ Y
inst✝¹ : f.IsDominant
g : Y ⤏ Z
inst✝ : g.IsDominant
⊢ (f.comp g.representative.toRationalMap).IsDominant
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2.refine_3
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV✝ : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
hU : (D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x) ∈ D.map k.hom ⁻¹ᵁ U
hV : ⟨(D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x), hU⟩ ∈ ↑V
⊢ ((opensDiagram D i U).map f) x ∈ V

Tactic:
convert! hV

Goal state after:
case e'_1
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV✝ : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
hU : (D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x) ∈ D.map k.hom ⁻¹ᵁ U
hV : ⟨(D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x), hU⟩ ∈ ↑V
⊢ ((opensDiagram D i U).map f) x = ⟨(D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x), hU⟩
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
⊢ @UniversallyInjective ≤ diagonal @Surjective

Tactic:
intro X

Goal state after:
case a
X : Scheme
⊢ @UniversallyInjective X ≤ diagonal @Surjective
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
⊢ diagonal @Surjective ≤ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x

Tactic:
intro X

Goal state after:
case a
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y),
    diagonal (@Surjective) f → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : f x₁ = f x₂
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t) = x₂
⊢ x₁ = x₂

Tactic:
← ht₁,

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : f x₁ = f x₂
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t) = x₂
⊢ (pullback.fst f f) ((pullback.diagonal f) t) = x₂
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case h
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := ⋯
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := ⋯
S₂ : Finset (BasicConstructibleSetData R) := ⋯
x : BasicConstructibleSetData (Localization.Away c)
hx : x ∈ T₁
k : Fin x.n
⊢ ⋃ i, coeff(e.val i) ⊆ {1} ∪ ⋃ i, coeff(e.val i)

Tactic:
exact Set.subset_union_right

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
⊢ TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (X.directedAffineCover.f i))

Tactic:
convert! X.isBasis_affineOpens
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

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

Tactic:
apply (𝒰.f j).injective
      dsimp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply]
      simp [xj, h2]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
inst✝⁶ : IsCofiltered I
i j : I
R : CommRingCat
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝² : ∀ (i : I), CompactSpace ↥((D ⋙ Scheme.Spec).obj i)
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
inst✝ : IsAffine c.pt
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : (D ⋙ Scheme.Spec).obj i ⟶ Spec S
b : (D ⋙ Scheme.Spec).obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
⊢ ∃ k hik hjk, (D ⋙ Scheme.Spec).map hik ≫ a = (D ⋙ Scheme.Spec).map hjk ≫ b

Tactic:
obtain ⟨a, rfl⟩ := Spec.map_surjective a

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
inst✝⁶ : IsCofiltered I
i j : I
R : CommRingCat
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝² : ∀ (i : I), CompactSpace ↥((D ⋙ Scheme.Spec).obj i)
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
inst✝ : IsAffine c.pt
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
b : (D ⋙ Scheme.Spec).obj j ⟶ Spec S
hb : t.app j = b ≫ Spec.map φ
a : S ⟶ Opposite.unop (D.obj i)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ b
ha : t.app i = Spec.map a ≫ Spec.map φ
⊢ ∃ k hik hjk, (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ b
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
⊢ { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
        f := fun x ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }.presieve₀ ∈
    (precoverage P).coverings W

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩
    · obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₂ f) x
      use i
      exact (mem_range_iff_of_surjective ((𝒰.pullback₂ f).f _) _
        ((PreservesPullback.iso (Over.forget S) ((𝒰.f _).asOver S) (f.asOver S)).inv)
        (PreservesPullback.iso_inv_snd _ _ _) x).mp hy
    · dsimp only
      rw [← Over.forget_map, ← PreservesPullback.iso_hom_snd, P.cancel_left_of_respectsIso]
      exact P.pullback_snd _ _ (𝒰.map_prop j)

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
this : ∀ i ∈ s, IsOpen (t i)
⊢ ⋃ i, ⋃ (h : i ∈ s), f i '' ↑((fun i hi ↦ { carrier := t i, is_open' := ⋯ }) i h) = U

Tactic:
simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]

Goal state after:
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 𝒰
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
j✝ : J
⊢ (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫ d.transitionMap (hij ≫ hjk)).left =
    (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
        (MorphismProperty.Over.mapComp ⊤ ⋯ ⋯ (Cover.trans 𝒰 (hij ≫ hjk)) ⋯).hom.app (d.cocone i).pt ≫
          (MorphismProperty.Over.map ⊤ ⋯).map (d.transitionMap hij) ≫ d.transitionMap hjk).left

Tactic:
simp [← Functor.map_comp_assoc, cocone_ι_transitionMap, pullback.map_comp_assoc]

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

Goal state before:
pp: case pos
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝¹ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
k : Fin n
h✝ : k = j
w✝ : ℕ
⊢ Polynomial.coeff 0 w✝ ∈ ↑(coeffSubmodule R₀ c)

Tactic:
exact zero_mem _

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

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
this : (c.val j).degree.succ ≠ 0
⊢ (c.val l).coeff m ∈ coeffSubmodule R₀ c

Tactic:
exact Submodule.subset_span (.inr (Set.mem_iUnion_of_mem l ⟨m, rfl⟩))

Goal state after:
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).c₆ = f W.c₆

Tactic:
simp only [c₆, map_b₂, map_b₄, map_b₆]

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ -f W.b₂ ^ 3 + 36 * f W.b₂ * f W.b₄ - 216 * f W.b₆ = f (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
h : W.c₄ = 0
⊢ W.j = 0

Tactic:
rw [j_eq_zero_iff', h, zero_pow three_ne_zero]

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

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ (n + 1) ^ numBound k₁ D₁ (n + 1) * degBound k₁ D₁ n ≤
    numBound k₂ D₂ (n + 1) ^ numBound k₂ D₂ (n + 1) * degBound k₂ D₂ n

Tactic:
refine Nat.mul_le_mul (Nat.pow_self_mono (numBound_mono hk _ hD)) (degBound_le_degBound hk _
      fun i hi ↦ hD _ (hi.trans n.lt_succ_self))

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
⊢ W.Equation x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0

Tactic:
rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]
  congr! 1
  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
⊢ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y - (-y - W.a₁ * x - W.a₃) ≠ 0)

Tactic:
congr! 3

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ ↑1⁻¹ ^ 6 * (W.a₆ + x * W.a₄ + x ^ 2 * W.a₂ + x ^ 3 - y * W.a₃ - y ^ 2 - x * y * W.a₁) = 0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    ↑1⁻¹ ^ 6 * (W.a₆ + x * W.a₄ + x ^ 2 * W.a₂ + x ^ 3 - y * W.a₃ - y ^ 2 - x * y * W.a₁) = 0 ∧
      (1 ^ 3 * (W.a₃ + x * W.a₁ + 2 * y) ≠ 0 ∨
        1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * x ^ 2 - 2 * 0 * y) ≠ 0)

Tactic:
congr! 3

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

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)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

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

Tactic:
sub_sub,

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