mathlib-initiative/mathlib-tactics huggingface dataset:
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
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
this : ∀ {X : Scheme} (f : X ⟶ Y), P f → IsAffine X → P (f ≫ g)
hX : ¬IsAffine X
⊢ P (f ≫ g)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover]
      intro i
      rw [← Category.assoc]
      exact this _ (comp_of_isOpenImmersion _ _ _ hf) inferInstance

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

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsIso (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f))

Tactic:
refine @IsIso.of_isIso_comp_right _ _ _ _ _ _ (X.presheaf.map
    (eqToHom (Scheme.toSpecΓ_preimage_basicOpen _ _).symm).op) _ ?_
  rw [ConcreteCategory.isIso_iff_bijective]
  apply +allowSynthFailures IsLocalization.bijective
  · exact StructureSheaf.IsLocalization.to_basicOpen _ _
  · refine isLocalization_basicOpen_of_qcqs ?_ ?_ _
    · exact isCompact_univ
    · exact isQuasiSeparated_univ
  · simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, RingHom.algebraMap_toAlgebra,
      ← Functor.map_comp]

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
⊢ ↑V ≤ ⨆ f, X.basicOpen ↑f

Tactic:
exact fun x hxV ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨_, _, rfl⟩, hxr ⟨x, hxV⟩⟩

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
this : Ideal.span (Set.range r) = ⊤
⊢ I.ideal V ≤ J.ideal V

Tactic:
have inst := V.2.isLocalization_basicOpen

Goal state after:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
this : Ideal.span (Set.range r) = ⊤
inst : ∀ (f : ↑Γ(X, ↑V)), IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ I.ideal V ≤ J.ideal V
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
y : ↥(Spec R)
hsub : f y ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑⊤
⊢ ringKrullDim ↑(X.presheaf.stalk (f y)) = ↑(coheight (f y))

Tactic:
coheight_eq_of_isOpenImmersion,

Goal state after:
case inr
X : Scheme
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
y : ↥(Spec R)
hsub : f y ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑⊤
⊢ ringKrullDim ↑(X.presheaf.stalk (f y)) = ↑(coheight y)
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsIso (Spec.map f) ↔ IsIso f

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

Goal state after:
R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ IsIso f
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
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
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
f : Spec S ⟶ Spec R
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

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
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ P (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X : Scheme
I✝ : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
I : Ideal ↑Γ(X, ↑U)
hx : x ∈ PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' PrimeSpectrum.zeroLocus ↑I)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')

Tactic:
rw [← vanishingIdeal_closure, e]

Goal state after:
case a
X : Scheme
I✝ : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
I : Ideal ↑Γ(X, ↑U)
hx : x ∈ PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' PrimeSpectrum.zeroLocus ↑I)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I))
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
X Y : Scheme
f✝ : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↥(Spec S)
hX : IsAffine (Spec S)
f : Spec S ⟶ Spec R
hf : P f
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↥(Spec S)
hX : IsAffine (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
S R : CommRingCat
f : Spec R ⟶ Spec S
inst✝ : QuasiCompact f
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst✝ : QuasiCompact (Spec.map φ)
⊢ ↑(ker (Spec.map φ)).support ⊆ closure (Set.range ⇑(Spec.map φ))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case mp
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
wlog hY : IsAffine Y
    · intro h
      rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := affineLocally Q)
        _ (iSup_affineOpens_eq_top _)]
      intro U
      have : IsAffine (f ⁻¹ᵁ U) := hf.isAffine_preimage U U.2
      rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q),
        morphismRestrict_appTop, CommRingCat.hom_comp, hQ.respectsIso.cancel_right_isIso]
      apply h
      rw [Scheme.Opens.ι_image_top]
      exact U.2
    intro h
    have : IsAffine X := isAffine_of_isAffineHom f
    rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q)]
    exact h ⊤ (isAffineOpen_top Y)

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

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ IsAffineOpen (U ⊓ V)

Tactic:
have : IsAffine _ := hU

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this : IsAffine ↑U
⊢ IsAffineOpen (U ⊓ V)
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: ⊢ OfLocalizationSpanTarget @FiniteType

Tactic:
by
  introv R hs H
  algebraize [f]
  replace H : ∀ r ∈ s, Algebra.FiniteType R (Localization.Away (r : S)) := by
    intro r hr; simp_rw [RingHom.FiniteType] at H; convert! H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl
  exact Algebra.FiniteType.of_span_eq_top_target s hs H

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

Goal state before:
pp: case refine_1
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
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage

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:
· let Q' : ObjectProperty CommRingCat.{u} := fun S ↦
      ∃ R, (R ∈ Set.range fun U ↦ Γ(X, U)) ∧ ∃ (f : R ⟶ S), f.hom.FiniteType
    have : Q'.EssentiallySmall := CommRingCat.essentiallySmall_of_finiteType fun S ↦ id
    suffices ObjectProperty.EssentiallySmall.{u} (· ∈ Set.range (Opposite.unop ∘ F.obj)) by
      rw [← ObjectProperty.essentiallySmall_unop_iff]
      refine .of_le (Q := .isoClosure (· ∈ Set.range (Opposite.unop ∘ F.obj))) ?_
      exact fun R ⟨S, e⟩ ↦ ⟨_, ⟨S, rfl⟩, ⟨e.some.unop⟩⟩
    refine CommRingCat.essentiallySmall_of_localizationAway (Q := Q'.isoClosure) ?_
    rintro _ ⟨S, rfl⟩
    have (q : Spec (F.obj S).unop) : ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧
        Q' Γ(Spec (F.obj S).unop, PrimeSpectrum.basicOpen f) := by
      obtain ⟨_, ⟨U, hU, rfl⟩, hqU, -⟩ :=
        X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ <| S.hom q) isOpen_univ
      obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hqf, hfU⟩ :=
        PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hqU (S.hom ⁻¹ᵁ U).isOpen
      have : LocallyOfFiniteType S.hom := hP _ S.prop
      exact ⟨f, hqf, _, ⟨U, rfl⟩, S.hom.appLE _ _ hfU,
        (S.hom.finiteType_appLE hU (.Spec_basicOpen _)) _⟩
    choose f hqf hf using this
    refine ⟨Set.range f, PrimeSpectrum.iSup_basicOpen_eq_top_iff.mp ?_, Set.forall_mem_range.mpr ?_⟩
    · exact top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, hqf _⟩
    · dsimp
      exact fun q ↦ ⟨_, hf q, ⟨(IsLocalization.algEquiv (.powers (f q)) _
        ((Spec.structureSheaf _).obj.obj (op _))).toRingEquiv.toCommRingCatIso⟩⟩

Goal state after:
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)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ (zeroLocus {(↑C).f})ᶜ ∩ zeroLocus ↑(RingHom.ker (Ideal.Quotient.mk I)) =
    (zeroLocus {(↑C).f})ᶜ ∩ zeroLocus (Set.range (↑C).g)

Tactic:
Ideal.mk_ker,

Goal state after:
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ (zeroLocus {(↑C).f})ᶜ ∩ zeroLocus ↑I = (zeroLocus {(↑C).f})ᶜ ∩ zeroLocus (Set.range (↑C).g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ IsDominant (Over.Hom.left (equalizer.lift ι' ?m.149 ≫ equalizer.ι f' g'))

Tactic:
equalizer.lift_ι

Goal state after:
W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ IsDominant (Over.Hom.left ι')
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this✝² : IsSeparated Y'.hom
this✝¹ : IsDominant (Over.Hom.left (equalizer.ι f' g'))
this✝ : Surjective (Over.Hom.left (equalizer.ι f' g'))
this : IsIso (Over.Hom.left (equalizer.ι f' g'))
⊢ f = g

Tactic:
← cancel_epi (equalizer.ι f' g').left

Goal state after:
W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this✝² : IsSeparated Y'.hom
this✝¹ : IsDominant (Over.Hom.left (equalizer.ι f' g'))
this✝ : Surjective (Over.Hom.left (equalizer.ι f' g'))
this : IsIso (Over.Hom.left (equalizer.ι f' g'))
⊢ Over.Hom.left (equalizer.ι f' g') ≫ f = Over.Hom.left (equalizer.ι f' g') ≫ g
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: R S : CommRingCat
inst✝ : Subsingleton ↥(Spec S)
f : Spec R ⟶ Spec S
g : Spec S ⟶ Spec R
hg : g ≫ f = 𝟙 (Spec S)
⊢ IsClosedImmersion g

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
R S : CommRingCat
inst✝ : Subsingleton ↥(Spec S)
g : Spec S ⟶ Spec R
φ : S ⟶ R
hg : g ≫ Spec.map φ = 𝟙 (Spec S)
⊢ IsClosedImmersion g
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
n : ℕ
hn : N ≤ n
⊢ ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) =
    ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) (I n))

Tactic:
iInf_subtype'

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 : ℕ
hn : N ≤ n
⊢ ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) =
    ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I n))
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
f : Spec S ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
φ : R ⟶ S
hf : LocallyOfFinitePresentation (Spec.map φ)
inst✝ : QuasiCompact (Spec.map φ)
⊢ IsLocallyConstructible (⇑(Spec.map φ) '' s)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : CommRingCat
inst✝¹ : IsLocallyNoetherian (Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst✝ : LocallyOfFiniteType f
⊢ id (IsLocallyNoetherian (Spec S))

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
R : CommRingCat
inst✝¹ : IsLocallyNoetherian (Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
⊢ id (IsLocallyNoetherian (Spec S))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X✝ Y✝ : Scheme
f✝¹ : X✝ ⟶ Y✝
X Y : Scheme
f✝ : X ⟶ Y
R S : CommRingCat
f : Spec S ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
f : Spec S ⟶ Spec K
⊢ UniversallyOpen f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
⊢ UniversallyOpen (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: Z S✝ : Scheme
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
Z S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ IsIntegralHom (Spec.map φ) → topologically (@IsClosedMap) (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: 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

Tactic:
have inst : IsAffine X := isAffine_of_isAffineHom f
    rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv]
    exact this _ inferInstance inferInstance ⟨_, rfl⟩

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsClosedImmersion),
    HasAffineProperty.iff_of_isAffine (P := @IsFinite),
    RingHom.surjective_iff_epi_and_finite, @and_comm (Epi _), ← and_assoc]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Epi (Scheme.Hom.appTop f) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
f : Spec R ⟶ Spec S
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
φ : S ⟶ R
⊢ IsFinite (Spec.map φ) ↔ LocallyOfFiniteType (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

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

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ IsOpen s
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j✝ : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ f j₁ = f j₂

Tactic:
refine (hf j₂).hom_ext ?_ (by simp [f])

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j✝ : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ f j₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂