mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ ↑U ⊓ ↑V ≤ ↑V ⊓ ↑U

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ Set.range ⇑(↑U ⊓ ↑V).ι ⊆ ↑↑V

Tactic:
by simp

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
⊢ IsAffineHom (f ≫ g)

Tactic:
by
  constructor
  intro U hU
  rw [Scheme.Hom.comp_base, Opens.map_comp_obj]
  apply IsAffineHom.isAffine_preimage
  apply IsAffineHom.isAffine_preimage
  exact hU

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ ↑i ≤ ↑i ⊓ ↑i

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑i ⊓ ↑i)

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑↑i

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯) =
    I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈ ↑↑⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (pullback.fst f g) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.x ∧ (pullback.snd f g) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.y

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ Scheme.Opens.ι (PrimeSpectrum.basicOpen ↑i) ''ᵁ ⊤ = PrimeSpectrum.basicOpen ↑i

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑U ⊓ ↑V)

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑↑U

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥Y), ∃ U, x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ IsAffineHom f

Tactic:
choose U hxU hU hfU using H
  rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]
  · exact hfU
  · exact top_le_iff.mp (fun x _ ↦ by simpa using ⟨x, hxU x⟩)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
f : R →+* S
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
hf : f.EssFiniteType
⊢ (IsLocalRing.ResidueField.map f).EssFiniteType

Tactic:
by
  refine .of_comp (IsLocalRing.residue R) ?_
  rw [IsLocalRing.ResidueField.map_comp_residue]
  exact .comp hf (FiniteType.of_surjective _ <| IsLocalRing.residue_surjective).essFiniteType

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.subschemeCover.f U ''ᵁ ⊤ = I.subschemeι ⁻¹ᵁ ↑U

Tactic:
by simp

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 ⋯
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv

Tactic:
replace this := Scheme.Hom.congr_app this U

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.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
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.subschemeι ⁻¹ᵁ ↑U = I.subschemeCover.f U ''ᵁ ⊤

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
e : CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ ↑U) :=
  (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).symm ≪≫
    (Hom.appIso (I.subschemeCover.f U) ⊤).symm ≪≫ Functor.mapIso I.subscheme.presheaf (eqToIso ⋯).op
⊢ RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U

Tactic:
RingHom.ker_equiv_comp,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
e : CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ ↑U) :=
  (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).symm ≪≫
    (Hom.appIso (I.subschemeCover.f U) ⊤).symm ≪≫ Functor.mapIso I.subscheme.presheaf (eqToIso ⋯).op
⊢ RingHom.ker (Ideal.Quotient.mk (I.ideal U)) = I.ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
x✝ : J.subschemeCover.openCover.I₀
⊢ J.subschemeCover.openCover.f x✝ ≫ inclusion h ≫ I.subschemeι = J.subschemeCover.openCover.f x✝ ≫ J.subschemeι

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝ : I.subschemeCover.openCover.I₀
⊢ I.subschemeCover.openCover.f x✝ ≫ inclusion ⋯ = I.subschemeCover.openCover.f x✝ ≫ 𝟙 I.subscheme

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
h₁ : I ≤ J
h₂ : J ≤ K
x✝ : K.subschemeCover.openCover.I₀
⊢ K.subschemeCover.openCover.f x✝ ≫ inclusion h₂ ≫ inclusion h₁ = K.subschemeCover.openCover.f x✝ ≫ inclusion ⋯

Tactic:
by simp

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

Goal state before:
pp: 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
h :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ ↑⟨f ⁻¹ᵁ U, ⋯⟩ ≤ f ⁻¹ᵁ ↑⟨U, hU⟩

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
he : Hom.app f ↑U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)
⊢ (Hom.ker f).ideal U ≤ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑U ≫ e.hom))

Tactic:
refine (IdealSheafData.ideal_ofIdeals_le _ _).trans_eq
    (RingHom.ker_equiv_comp _ e.commRingCatIsoToRingEquiv).symm

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ (Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion ⋯) ≫ ⊥.subschemeι = 𝟙 X

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ RingHom.ker (CommRingCat.Hom.hom (app f ↑U)) ≤ (ker f).ideal U

Tactic:
by simp

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

Goal state before:
pp: 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
this : IsAffine ↑V
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
⊢ X.homOfLE ⋯ ≫ V.ι = X.homOfLE ⋯ ≫ U.ι

Tactic:
by simp

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

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
I : Y.IdealSheafData
⊢ (𝟭 Y.IdealSheafData).obj I = ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor).obj I

Tactic:
by simp

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

Goal state before:
pp: case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
this : IsAffineOpen (Scheme.Hom.opensRange (pullback.fst f₁ f₂ ≫ f₁))
⊢ IsAffine (pullback f₁ f₂)

Tactic:
change IsAffine _ at this

Goal state after:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
this : IsAffine ↑(Scheme.Hom.opensRange (pullback.fst f₁ f₂ ≫ f₁))
⊢ IsAffine (pullback f₁ f₂)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
inst✝ : IsAffineHom (pullback.diagonal (terminal.from X))
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ U ≤ terminal.from X ⁻¹ᵁ ⊤

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
inst✝ : IsAffineHom (pullback.diagonal (terminal.from X))
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ V ≤ terminal.from X ⁻¹ᵁ ⊤

Tactic:
by simp

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

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

Tactic:
obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f

Goal state after:
R : CommRingCat
inst✝¹ : JacobsonSpace ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
⊢ JacobsonSpace ↥(Spec S)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
by simp

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

Goal state before:
pp: X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.comap g).subschemeι ≫ 𝟙 Y = (I.comapIso g).hom ≫ pullback.fst g I.subschemeι

Tactic:
by simp

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

Goal state before:
pp: Z : Scheme
I : Z.IdealSheafData
⊢ I.comap (𝟙 Z) = I

Tactic:
by
  rw [comap, ← Scheme.Hom.ker_comp_of_isIso (inv (pullback.snd _ _)),
    pullback_inv_snd_fst_of_left_isIso, IsIso.inv_id, Category.comp_id, ker_subschemeι]

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

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
by simp

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

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ i ≫ 𝟙 Y = Hom.toImage i ≫ Hom.imageι i

Tactic:
by simp

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

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (pullback.lift iX Zf h)
⊢ iX ≫ 𝟙 X = pullback.lift iX Zf h ≫ pullback.fst f iY

Tactic:
by simp

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

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (pullback.lift iX Zf h)
⊢ IsPullback iX Zf f iY

Tactic:
simpa using (IsPullback.of_vert_isIso (show CommSq iX (pullback.lift iX Zf h)
      (𝟙 X) (pullback.fst _ _) from ⟨by simp⟩)).paste_vert (IsPullback.of_hasPullback f iY)

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

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
⊢ pullback.lift iX Zf h ≫ pullback.fst f iY = iX

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ({ obj := fun I ↦ op (MorphismProperty.Over.mk ⊤ I.subschemeι ⋯),
            map := fun {I J} h ↦ (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op, map_id := ⋯,
            map_comp := ⋯ } ⋙
          (MorphismProperty.Over.forget @IsClosedImmersion ⊤ X).op ⋙ X.kerFunctor).obj
      I =
    (𝟭 X.IdealSheafData).obj I

Tactic:
by simp

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = 𝟙 (Scheme.Hom.ker i₂)

Tactic:
by simp

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = 𝟙 (Scheme.Hom.ker i₁)

Tactic:
by simp

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
h : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
⊢ lift i₁ i₂ ⋯ ≫ i₁ = i₂

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : ↑X.affineOpens
⊢ (I.comap f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso f ↑U).inv) (I.ideal ⟨f ''ᵁ ↑U, ⋯⟩)

Tactic:
refine (ker_ideal_of_isPullback_of_isOpenImmersion _ _ _ _
    (IsPullback.of_hasPullback f I.subschemeι) U).trans ?_

Goal state after:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : ↑X.affineOpens
⊢ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso f ↑U).inv) ((Hom.ker I.subschemeι).ideal ⟨f ''ᵁ ↑U, ⋯⟩) =
    Ideal.comap (CommRingCat.Hom.hom (Hom.appIso f ↑U).inv) (I.ideal ⟨f ''ᵁ ↑U, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ W i ≤ 𝒰.f i ⁻¹ᵁ ⊤

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ Hom.liftCoborder f ≫ (Hom.coborderRange f).ι = Hom.toImage f ≫ Hom.imageι f

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0

Tactic:
have h1 (i : 𝒰.I₀) : ∃ n, (res i) (φ (s ^ n * g)) = 0 := by
    obtain ⟨n, hn⟩ := exists_of_res_zero_of_qcqs_of_top (s := ((res i) (φ s))) (h0 i)
    exact ⟨n, by rwa [map_mul, map_mul, map_pow, map_pow]⟩

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
h1 : ∀ (i : 𝒰.I₀), ∃ n, (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0
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
ht : Ideal.span ↑t = ⊤
⊢ Ideal.span ↑{∑ g ∈ s.attach, g' g * h' g - 1} = Ideal.span {∑ g ∈ s.attach, g' g * h' g - 1}

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
⊢ ⨆ (_ : PUnit.{0}), ⊤ = ⊤

Tactic:
by simp

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

Goal state before:
pp: X Y S : Scheme
inst✝⁶ : X.Over S
inst✝⁵ : Y.Over S
inst✝⁴ : IsReduced X
inst✝³ : IsSeparated (Y ↘ S)
f g : X ⟶ Y
inst✝² : Scheme.Hom.IsOver f S
inst✝¹ : Scheme.Hom.IsOver g S
W : Scheme
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
⊢ f ≫ Y ↘ S = g ≫ Y ↘ S

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible S.toSet
⊢ ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ ⊤

Tactic:
by simp

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

Goal state before:
pp: X✝ Y✝ Z X Y : Scheme
inst✝² : Subsingleton ↥Y
inst✝¹ : X.Over Y
f : Y ⟶ X
inst✝ : Scheme.Hom.IsOver f Y
⊢ f ≫ X ↘ Y = 𝟙 Y

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ ∀ (i : ↑↑t), IsCompact (zeroLocus {↑i})ᶜ

Tactic:
exact fun _ ↦ by simpa using isCompact_basicOpen _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsNoetherianRing ↑R
⊢ ⨆ i, ↑⟨⊤, ⋯⟩ = ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_1
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ IsLocallyNoetherian X

pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X

Tactic:
· exact (isLocallyNoetherian_iff_openCover 𝒰).mpr inferInstance

Goal state after:
case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X✝ Y✝ P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ Y.fromSpecResidueField y ≫ g = Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y)

Tactic:
by simp

Goal state after: