mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
apply +allowSynthFailures hasPullback_of_left_iso

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ IsIso (D.f' i j)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
          y)

Tactic:
simp_rw [← D.ι_isoCarrier_inv]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ (gluedCover 𝒰).glued ⟶ X

Tactic:
fapply Multicoequalizer.desc
  · exact fun x => 𝒰.f x
  rintro ⟨x, y⟩
  change pullback.fst _ _ ≫ _ = ((pullbackSymmetry _ _).hom ≫ pullback.fst _ _) ≫ _
  simpa using! pullback.condition

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)

Tactic:
simp_rw [Category.assoc, cocycle_snd_snd 𝒰 f g i j k]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
⊢ IsOpenImmersion f

Tactic:
apply +allowSynthFailures IsOpenImmersion.of_isIso_stalkMap

Goal state after:
case hf
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
⊢ Topology.IsOpenEmbedding ⇑f

case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
⊢ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingPair
⊢ Mono ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))

Tactic:
mono_iff_injective

Goal state after:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingPair
⊢ Function.Injective ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f ↔ Q f

Tactic:
rw [iff_of_openCover (P := P) (Scheme.coverOfIsIso.{0} (𝟙 Y))]

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 Y)).toPreZeroHypercover.1), Q ((Scheme.coverOfIsIso (𝟙 Y)).pullbackHom f i)) ↔ Q f
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₂
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : f x ⤳ y
a : α
ha : a ∈ closure[inst✝¹] {x}
hay : f a = y
⊢ ⟨y, hy⟩ ∈ s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {⟨x, hx⟩}

Tactic:
exact ⟨⟨a, by simp [hay, hy]⟩, by simpa [closure_subtype], by simpa⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝² : M.Over S
f : T ⟶ S
inst✝¹ : MonObj (M.asOver S)
inst✝ : IsCommMonObj (M.asOver S)
⊢ IsCommMonObj ((pullback (M ↘ S) f).asOver T)

Tactic:
by
  unfold asOver OverClass.asOver at *; exact Over.isCommMonObj_mk_pullbackSnd

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
⊢ IsZariskiLocalAtSource P.diagonal

Tactic:
let g {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) :=
    pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) (by simp) (by simp)
  refine IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)
  · change P _
    apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance
    rw [← pullback.comp_diagonal]
    apply IsZariskiLocalAtSource.comp
    exact hf
  · change P _
    refine IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_
    rw [pullback.comp_diagonal]
    exact RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ P).IsLocal

Tactic:
constructor
  · exact sourceAffineLocally_respectsIso P h₁
  · intro X Y _ f r H
    rw [sourceAffineLocally_morphismRestrict]
    intro U hU
    have : X.basicOpen (f.appLE ⊤ U (by simp) r) = U := by
      simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]
      rw [Scheme.basicOpen_res]
      simpa using hU
    rw [← f.appLE_congr (by simp [Scheme.Hom.appLE]) rfl this (fun f => P f.hom),
      IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2 _ r]
    simp only [CommRingCat.hom_ofHom]
    apply +allowSynthFailures h₂
    exact H U
  · introv hs hs' U
    apply h₃ _ _ hs
    intro r
    simp_rw [sourceAffineLocally_morphismRestrict] at hs'
    have := hs' r ⟨X.basicOpen (f.appLE ⊤ U le_top r.1), U.2.basicOpen (f.appLE ⊤ U le_top r.1)⟩
      (by simp [Scheme.Hom.appLE])
    rwa [IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2, CommRingCat.hom_ofHom,
      ← h₁.isLocalization_away_iff] at this

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsQuasiSeparated ↑U

Tactic:
isQuasiSeparated_iff_quasiSeparatedSpace

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ QuasiSeparatedSpace ↑↑U

case hs
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsOpen ↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
s : Set ↑Γ(X, U)
⊢ X.zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical ↑Γ(X, U))

Tactic:
by
  simp [Scheme.zeroLocus_def, ← Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact hU,
    ← mem_nilradical, Set.subset_def]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ ↑m' * y = 0

Tactic:
← hm',

Goal state after:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ ↑m' * y = y * ↑m'
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI : I.height = 0
p : Ideal R
w✝ : p.IsPrime
hIp : I ≤ p
hp0 : p.height = ↑0
⊢ I = ⊥

Tactic:
CharP.cast_eq_zero,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI : I.height = 0
p : Ideal R
w✝ : p.IsPrime
hIp : I ≤ p
hp0 : p.height = 0
⊢ I = ⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0

Tactic:
obtain ⟨V, hxV, iU, iV, (e' : (X.presheaf.map iU.op) (s ^ n) = (X.presheaf.map iV.op) 0)⟩ :=
    X.presheaf.germ_eq x hxU hxU _ 0 e

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) (s ^ n) = (ConcreteCategory.hom (X.presheaf.map iV.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case component_integral
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : IsDomain ↑Γ(Y, f ''ᵁ U)
⊢ IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Tactic:
exact (asIso <| f.app (f ''ᵁ U) :
    Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _

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

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ IsOpenMap ⇑f

Tactic:
intro U hU
    convert! (⨆ i, ((𝒰.f i ≫ f) ''ᵁ (𝒰.f i ⁻¹ᵁ ⟨U, hU⟩))).2
    ext x
    exact ⟨fun ⟨x, _, _⟩ ↦ by have := 𝒰.exists_eq x; simp; grind, by simp; grind⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ map ((Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).isoSpec.inv =
    map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Tactic:
Scheme.isoSpec_Spec_inv,

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ map ((Spec R).presheaf.germ ⊤ x trivial) ≫ map (Scheme.ΓSpecIso R).inv =
    map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
this✝ : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫ (ΓSpecIso (X.presheaf.stalk x)).inv ≫ Hom.appLE (Spec.map f) ⊤ ⊤ ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
simp_rw [← Opens.map_top (Spec.map f).base]

Goal state after:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
this✝ : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
⊢ ⨅ i, ker (𝒰.f i ≫ f) = ker f

Tactic:
refine le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f)
  refine iInf_le_iff.mpr fun I hI U ↦ ?_
  rw [← f.iInf_ker_openCover_map_comp_apply 𝒰, le_iInf_iff]
  exact fun i ↦ hI i U

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: K : Type u
inst✝ : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
⊢ Spec.map (descResidueField (stalkClosedPointTo f)) ≫ X.fromSpecResidueField (f (closedPoint K)) = f

Tactic:
X.descResidueField_fromSpecResidueField,

Goal state after:
K : Type u
inst✝ : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑(CommRingCat.of K))) = f
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsAffine ↑(X.toSpecΓ ⁻¹ᵁ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩)

Tactic:
rw [Scheme.toSpecΓ_preimage_basicOpen]

Goal state after:
case refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsAffine ↑(X.basicOpen ↑i)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J ≤ I.map f ↔ J.comap f ≤ I

Tactic:
constructor
  · intro H
    rw [← I.ker_subschemeι, ← pullback.lift_fst (f := f) (g := J.subschemeι) I.subschemeι
      ((I.subschemeι ≫ f).toImage ≫ inclusion H) (by simp)]
    exact Hom.le_ker_comp _ _
  · intro H
    have : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd _ _) ≫ J.subschemeι =
        I.subschemeι ≫ f := by simp [← pullback.condition]
    rw [map, ← J.ker_subschemeι, ← this]
    exact Hom.le_ker_comp _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
H : IsAffineOpen (f ⁻¹ᵁ ↑U)
⊢ (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.app f ↑U)) (I.ideal ⟨f ⁻¹ᵁ ↑U, H⟩)

Tactic:
have : RingHom.ker (I.subschemeObjIso ⟨_, H⟩).inv.hom = ⊥ :=
    RingHom.ker_coe_equiv (I.subschemeObjIso ⟨_, H⟩).symm.commRingCatIsoToRingEquiv

Goal state after:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
H : IsAffineOpen (f ⁻¹ᵁ ↑U)
this : RingHom.ker (CommRingCat.Hom.hom (I.subschemeObjIso ⟨f ⁻¹ᵁ ↑U, H⟩).inv) = ⊥
⊢ (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.app f ↑U)) (I.ideal ⟨f ⁻¹ᵁ ↑U, H⟩)
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
this : (Ideal.Quotient.mk I) (∑ g, g' g * h' g) = 1
⊢ ∑ x ∈ s.attach, (Ideal.Quotient.mk I) (g' x) * (Ideal.Quotient.mk I) (h' x) ∈ Ideal.span ↑t

Tactic:
refine Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
this : (Ideal.Quotient.mk I) (∑ g, g' g * h' g) = 1
g : ↥s
x✝ : g ∈ s.attach
⊢ (Ideal.Quotient.mk I) (g' g) ∈ ↑t
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderGeneralization s
hs' : IsConstructible s
⊢ IsClosed sᶜ

Tactic:
exact isClosed_of_stableUnderSpecialization_of_isConstructible hs.compl hs'.compl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
⊢ IsNilpotent ((algebraMap A (A ⊗[R] I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Subsingleton R
⊢ IsNilpotent ((algebraMap A (A ⊗[R] I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

case inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
⊢ IsNilpotent ((algebraMap A (A ⊗[R] I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
⊢ NoetherianSpace ↥X

Tactic:
apply TopologicalSpace.noetherian_univ_iff.mp
  let 𝒰 := X.affineCover.finiteSubcover
  rw [← 𝒰.iUnion_range]
  suffices ∀ i : 𝒰.I₀, NoetherianSpace (Set.range <| (𝒰.f i)) by
    apply NoetherianSpace.iUnion
  intro i
  have : IsAffine (𝒰.X i) := by
    rw [X.affineCover.finiteSubcover_X]
    apply Scheme.isAffine_affineCover
  let U : X.affineOpens := ⟨Scheme.Hom.opensRange (𝒰.f i), isAffineOpen_opensRange _⟩
  convert! noetherianSpace_of_isAffineOpen U.1 U.2
  apply IsLocallyNoetherian.component_noetherian

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: ⊢ geometrically IsIntegral = geometrically IsReduced ⊓ geometrically fun x ↦ IrreducibleSpace ↥x

Tactic:
← geometrically_inf

Goal state after:
⊢ geometrically IsIntegral = geometrically (IsReduced ⊓ fun x ↦ IrreducibleSpace ↥x)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X Y✝ : Scheme
f✝ : X ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme} [IsIntegral Y] [Subsingleton ↥Y] (f : Spec S ⟶ Y), (∃ K, Y = Spec K ∧ IsField ↑K) → UniversallyOpen f
hY : ¬∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f

pp: X Y✝ : Scheme
f✝ : X ⟶ Y✝
S : CommRingCat
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
f : Spec S ⟶ Y
hY : ∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f

Tactic:
· have inst : Subsingleton (Spec Γ(Y, ⊤)) := Y.isoSpec.inv.homeomorph.subsingleton
    exact (MorphismProperty.cancel_right_of_respectsIso _ _ Y.isoSpec.hom).mp
      (this _ ⟨_, rfl, isField_of_isIntegral_of_subsingleton _⟩)

Goal state after:
X Y✝ : Scheme
f✝ : X ⟶ Y✝
S : CommRingCat
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
f : Spec S ⟶ Y
hY : ∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)

Tactic:
by
    convert! this <;> rw [toSpecΓ_preimage_basicOpen]

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ Flat (Spec.map f) ∧ Surjective (Spec.map f) ↔ (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
HasRingHomProperty.Spec_iff (P := @Flat),

Goal state after:
R S : CommRingCat
f : R ⟶ S
⊢ (CommRingCat.Hom.hom f).Flat ∧ Surjective (Spec.map f) ↔ (CommRingCat.Hom.hom f).FaithfullyFlat
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
⊢ (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x = (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) y

Tactic:
nth_rw 2 [coeq_condition]

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
⊢ (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x = (ConcreteCategory.hom (F.map (f' ≫ coeqHom f f'))) y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
by
  constructor
  · intro h j j' x x' eq
    have : F.ιColimitType j x = F.ιColimitType j' x' := h eq
    rwa [ιColimitType_eq_iff_of_isFiltered] at this
  · intro h x x' eq
    obtain ⟨i, x, rfl⟩ := F.ιColimitType_jointly_surjective x
    obtain ⟨i', x', rfl⟩ := F.ιColimitType_jointly_surjective x'
    simp only [descColimitType_ιColimitType_apply] at eq
    obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
    rw [← F.ιColimitType_map f x, eq, F.ιColimitType_map]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
hw : w ∈ s
⊢ (if w ∈ s then D w else 0) = D w

Tactic:
simp [hw]

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✝¹ : AddCommGroup Y
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊔ D₂).restrict h = D₁.restrict h ⊔ D₂.restrict h

Tactic:
by
    ext x
    by_cases hx : x ∈ V
    <;> simp [locallyFinsuppWithin.restrict_apply, hx]

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✝¹ : AddCommGroup Y
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊓ D₂).restrict h = D₁.restrict h ⊓ D₂.restrict h

Tactic:
by
    ext x
    by_cases hx : x ∈ V
    <;> simp [locallyFinsuppWithin.restrict_apply, hx]

Goal state after: