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

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
⊢ P (f ≫ i)

Tactic:
wlog hZ : IsAffine Z generalizing X Y Z

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
⊢ P (f ≫ i)

P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
⊢ P (f ≫ i)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case surj
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1

Tactic:
intro z
    obtain ⟨n, y, e⟩ := exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated X U hU hU' f z
    refine ⟨⟨y, _, n, rfl⟩, ?_⟩
    simpa only [map_pow, Subtype.coe_mk, RingHom.algebraMap_toAlgebra, mul_comm z] using! e.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
z : ↥X
n : ℕ
hz : coheight z ≤ ↑n
⊢ ringKrullDim ↑(X.presheaf.stalk z) ≤ ↑n

Tactic:
ringKrullDim_stalk_eq_coheight z

Goal state after:
X : Scheme
z : ↥X
n : ℕ
hz : coheight z ≤ ↑n
⊢ ↑(coheight z) ≤ ↑n
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val '' Subtype.val ⁻¹' X.zeroLocus ↑(I.ideal U) = Subtype.val '' Subtype.val ⁻¹' I.supportSet

Tactic:
simp [Set.image_preimage_eq_inter_range, I.supportSet_inter]

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine Y → P f
hY : ¬IsAffine Y
⊢ P f

pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
⊢ P f

Tactic:
· rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
    intro U
    refine this (fun x ↦ ?_) U.2
    exact (hQi.arrow_mk_iso_iff (AlgebraicGeometry.morphismRestrictStalkMap f U x)).mpr (H x.val)

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
⊢ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ IsIso f✝ ↔ (IsOpenImmersion ⊓ @Surjective) f✝

Tactic:
isIso_iff_isOpenImmersion_and_surjective

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ IsOpenImmersion f✝ ∧ Surjective f✝ ↔ (IsOpenImmersion ⊓ @Surjective) f✝
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ (IsAffineOpen.isoSpec ⋯).hom ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    X.homOfLE h

Tactic:
IsAffineOpen.isoSpec_hom,

Goal state after:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ (↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    X.homOfLE h
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : IsEmpty ↥X
U : ↑Y.affineOpens
x : ↑Γ(Y, ↑U)
x✝ : x ∈ ⊤.ideal U
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
by simpa using Subsingleton.elim _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x₁ x₂ : ↥X
e : x₁ = x₂
⊢ residueFieldMap f x₁ ≫ (residueFieldCongr e).hom = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x₂

Tactic:
by
  subst e
  simp

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

Goal state before:
pp: case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))

Tactic:
apply hQl

Goal state after:
case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: ⊢ MorphismProperty.IsStableUnderBaseChange @Surjective

Tactic:
refine .mk' ?_
  introv hg
  simp only [surjective_iff, ← Set.range_eq_univ, Scheme.Pullback.range_fst] at hg ⊢
  rw [hg, Set.preimage_univ]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ Set.range ⇑I.gluedTo = ↑I.support

Tactic:
by
  refine subset_antisymm (Set.range_subset_iff.mpr fun x ↦ ?_) ?_
  · obtain ⟨ix, x : I.glueDataObj ix, rfl⟩ :=
      I.glueData.toGlueData.ι_jointly_surjective forget x
    change (I.glueData.ι _ ≫ I.gluedTo) x ∈ I.support
    rw [ι_gluedTo]
    exact ((I.range_glueDataObjι_ι_eq_support_inter ix).le ⟨_, rfl⟩).1
  · intro x hx
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
    obtain ⟨y, rfl⟩ := (I.range_glueDataObjι_ι_eq_support_inter ⟨U, hU⟩).ge ⟨hx, hxU⟩
    rw [← ι_gluedTo]
    exact ⟨_, rfl⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
this✝ :
  I.subschemeCover.f U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  Hom.app (I.subschemeCover.f U ≫ I.subschemeι) ↑U =
    Hom.app (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯) ↑U ≫
      (Spec (I.subschemeCover.X U)).presheaf.map (eqToHom ⋯).op
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv

Tactic:
simp only [Hom.comp_base, TopologicalSpace.Opens.map_comp_obj, Hom.comp_app,
    IsAffineOpen.fromSpec_app_self, eqToHom_op, Category.assoc, Hom.naturality_assoc,
    TopologicalSpace.Opens.map_top, ← ΓSpecIso_inv_naturality_assoc] at this

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
this✝ :
  I.subschemeCover.f U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  Hom.app I.subschemeι ↑U ≫ Hom.app (I.subschemeCover.f U) (I.subschemeι ⁻¹ᵁ ↑U) =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫
      (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).inv ≫
        (Spec (I.subschemeCover.X U)).presheaf.map
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map (eqToHom ⋯).unop).op ≫
          (Spec (I.subschemeCover.X U)).presheaf.map (eqToHom ⋯)
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P = @IsAffineHom ⊓ P'

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally (P := P),
    targetAffineLocally_affineAnd_eq_affineLocally,
    HasRingHomProperty.eq_affineLocally (P := P')]
  exact HasRingHomProperty.isLocal_ringHomProperty P'

Goal state after:
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
      (Localization.Away (f r)) _ (s₁ r) hn₁

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
⊢ ∀ (Y : CommRingCatᵒᵖ), ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ Y)

Tactic:
intro R
    refine ⟨.ofObj fun f : { f : Spec R.unop ⟶ X // P f } ↦ .mk _ f.1 f.2, inferInstance, ?_⟩
    refine fun S ⟨e⟩ ↦ ⟨_, .mk ⟨Spec.map e.inv.unop ≫ S.hom, ?_⟩,
      ⟨MorphismProperty.CostructuredArrow.isoMk e trivial trivial ?_⟩⟩
    · simp [← Spec.map_comp_assoc, F]
    · exact (P.cancel_left_of_respectsIso _ _).mpr S.prop

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

Goal state before:
pp: X Y Z : Scheme
I : X.IdealSheafData
J : Y.IdealSheafData
f : X ⟶ Y
H : J ≤ I.map f
⊢ Hom.ker J.subschemeι ≤ Hom.ker (I.subschemeι ≫ f)

Tactic:
by simpa using! H

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : ConstructibleSetData R
x✝¹ : BasicConstructibleSetData R
x✝ : x✝¹ ∈ ↑S
⊢ IsConstructible (zeroLocus (Set.range x✝¹.g))

Tactic:
rw [← isConstructible_compl]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : ConstructibleSetData R
x✝¹ : BasicConstructibleSetData R
x✝ : x✝¹ ∈ ↑S
⊢ IsConstructible (zeroLocus (Set.range x✝¹.g))ᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
S : ConstructibleSetData R
x✝¹ : BasicConstructibleSetData R
x✝ : x✝¹ ∈ ↑S
⊢ IsConstructible (zeroLocus {x✝¹.f})

Tactic:
rw [← isConstructible_compl]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
S : ConstructibleSetData R
x✝¹ : BasicConstructibleSetData R
x✝ : x✝¹ ∈ ↑S
⊢ IsConstructible (zeroLocus {x✝¹.f})ᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: case union
R : Type u_1
inst✝ : CommSemiring R
s✝ s : Set (PrimeSpectrum R)
hs : IsConstructible s
t : Set (PrimeSpectrum R)
ht : IsConstructible t
Hs : ∃ S, S.toSet = s
Ht : ∃ S, S.toSet = t
⊢ ∃ S, S.toSet = s ∪ t

Tactic:
| union s hs t ht Hs Ht =>

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
this : IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h)

Tactic:
exact .of_comp _ I.subschemeι

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

Goal state before:
pp: X✝ Y✝ Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
⊢ LocallyOfFiniteType f

Tactic:
by
  rw [HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType,
    ← and_iff_right (inferInstance : IsAffineHom f) (b := affineLocally _ _),
    ← targetAffineLocally_affineAnd_iff_affineLocally RingHom.finiteType_isLocal]
  rw [HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion] at h
  exact targetAffineLocally_affineAnd_le (RingHom.FiniteType.of_surjective _) _ h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
⊢ ∀ (m : ℕ), N ≤ m → I N = I m

Tactic:
intro n

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
⊢ N ≤ n → I N = I n
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: ⊢ @GeometricallyReduced = geometrically IsReduced

Tactic:
ext; exact geometricallyReduced_iff _

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

Goal state before:
pp: case pos
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
k : Fin n
hjk : k = j
⊢ (e.val j %ₘ e.val i).degree ≤ (ofLex e.degree).1 k

Tactic:
rw [hjk]

Goal state after:
case pos
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
k : Fin n
hjk : k = j
⊢ (e.val j %ₘ e.val i).degree ≤ (ofLex e.degree).1 j
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [ConcreteCategory.hom_ofHom, coe_eval₂Hom, eval₂_X]

Goal state after:
n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ Spec.map (φ ≫ CommRingCat.ofHom C) = Spec.map (CommRingCat.ofHom ((MvPolynomial.map (CommRingCat.Hom.hom φ)).comp C))

Tactic:
map_comp_C,

Goal state after:
case h₁
n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ Spec.map (φ ≫ CommRingCat.ofHom C) = Spec.map (CommRingCat.ofHom (C.comp (CommRingCat.Hom.hom φ)))
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
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
j j' : J
x : F.obj j
x' : F.obj j'
eq : c.ι j x = c.ι j' x'
⊢ c.ι (IsFiltered.max j j') ((ConcreteCategory.hom (F.map (leftToMax j j'))) x) =
    c.ι (IsFiltered.max j j') ((ConcreteCategory.hom (F.map (rightToMax j j'))) x')

Tactic:
by simpa only [c.ι_naturality_apply]

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
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ ((D₁ + D₂).restrict h) x = (D₁.restrict h + D₂.restrict h) x

Tactic:
by_cases hx : x ∈ V
    <;> simp [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✝ : Zero Y
f : locallyFinsuppWithin U Y
p : X
hp : p ∈ U
⊢ ∃ s ∈ 𝓝[f.support] p, s.Finite

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := f.supportLocallyFiniteWithinDomain p hp

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
⊢ ∃ s ∈ 𝓝[f.support] p, s.Finite
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ Scheme.Hom.resLE f V U ⋯ ≫ V.ι = U.ι ≫ g

Tactic:
← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_right)

Goal state after:
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ Scheme.Hom.resLE f V U ⋯ ≫ V.ι = Scheme.Hom.resLE g V U ⋯ ≫ V.ι
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z : Scheme
f : X.PartialMap Y
g : Y ⟶ Z
x : ↥X
hx : x ∈ (f.compHom g).domain
⊢ (f.compHom g).fromSpecStalkOfMem hx = f.fromSpecStalkOfMem hx ≫ g

Tactic:
by
  simp [fromSpecStalkOfMem]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ (Hom.toPartialMap f).fromSpecStalkOfMem trivial = X.fromSpecStalk x ≫ f

Tactic:
by
  simp [fromSpecStalkOfMem]

Goal state after: