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

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine ⟨α.opensRange, ⟨_, e⟩, ?_⟩

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst ∧
        l ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt},
            m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst →
              m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd → m = l }

Tactic:
intro s

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
⊢ { l //
    l ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt},
          m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd → m = l }
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
⊢ Set.range ⇑f ⊆ Set.range ⇑(⨆ i, U i).ι

Tactic:
by simpa using H

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ Set.range ⇑f ⊆ Set.range ⇑(⨆ i, U i).ι

Tactic:
by simpa using H

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
⊢ P = targetAffineLocally (AffineTargetMorphismProperty.of P)

Tactic:
by
    ext X Y f
    constructor
    · intro hf ⟨U, hU⟩
      exact IsZariskiLocalAtTarget.restrict hf _
    · intro hf
      exact P.of_zeroHypercover_target Y.affineCover
        fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h) ≫ pullback.fst fXZ fYZ =
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.fst fXZ fYZ

Tactic:
simp [f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h) ≫ pullback.snd fXZ fYZ =
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.snd fXZ fYZ

Tactic:
simp [f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
obtain ⟨i, rfl⟩ := (equivShrink J).symm.surjective i

Goal state after:
case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
j : J
xj : ↥(F.obj j)
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
⊢ (colimit.ι F ↓i) xi = (colimit.ι F j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : s.fst.base ≫ D.toTopGlueData.ι i = s.snd.base ≫ D.toTopGlueData.ι j
⊢ Set.range ⇑(ConcreteCategory.hom s.fst.base) ⊆
    ⇑(ConcreteCategory.hom (D.toTopGlueData.ι i)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.toTopGlueData.ι j))

Tactic:
simp only [mapGlueData_U, forget_obj]

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : s.fst.base ≫ D.toTopGlueData.ι i = s.snd.base ≫ D.toTopGlueData.ι j
⊢ Set.range ⇑(ConcreteCategory.hom s.fst.base) ⊆
    ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) ⁻¹'
      Set.range ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun f ↦ Y.basicOpen ↑f) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : 𝒰.toPreZeroHypercover.1
⊢ Y.basicOpen ↑i = Scheme.Hom.opensRange (𝒰.f i)

Tactic:
simp [𝒰]

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
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ ↑U ⊓ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) r) = ↑U

Tactic:
simpa using hU

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)

Tactic:
rw [quasiCompact_iff]
  refine ⟨fun H U hU => H U U.isOpen hU.isCompact, ?_⟩
  intro H U hU hU'
  obtain ⟨S, hS, rfl⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU', hU⟩
  simp only [Set.preimage_iUnion]
  exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ∀ (i : ↑Us), P ((V i).ι ≫ f ≫ U.ι)

Tactic:
intro s

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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
⊢ P ((V s).ι ≫ f ≫ U.ι)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
have := I.map_ideal_basicOpen_of_eq (V := X.affineBasicOpen g) f (Subtype.ext hfg.symm)

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this : Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen g)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)
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
x : ↥X
hxV : x ∈ ↑V
⊢ ∃ i r rU, X.basicOpen r = X.basicOpen rU ∧ ↑⟨x, hxV⟩ ∈ X.basicOpen r

Tactic:
obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp (hU.ge (Set.mem_univ x))

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
x : ↥X
hxV : x ∈ ↑V
i : ι
hi : x ∈ ↑(U i)
⊢ ∃ i r rU, X.basicOpen r = X.basicOpen rU ∧ ↑⟨x, hxV⟩ ∈ X.basicOpen r
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
⊢ ∀ f ∈ I.ideal V, x ∉ X.basicOpen f

Tactic:
intro s

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
⊢ s ∈ I.ideal V → x ∉ X.basicOpen s
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ Antitone support

Tactic:
intro I

Goal state after:
X : Scheme
I : X.IdealSheafData
⊢ ∀ ⦃b : X.IdealSheafData⦄, I ≤ b → b.support ≤ I.support
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsIso (Spec.map f) ↔ Function.Bijective ⇑(CommRingCat.Hom.hom f)

Tactic:
← ConcreteCategory.isIso_iff_bijective

Goal state after:
R S : CommRingCat
f : R ⟶ S
⊢ IsIso (Spec.map f) ↔ IsIso f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
H : ⊤ ≤ X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V
⊢ (ΓSpecIso Γ(X, ↑V)).inv ≫ Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.app F ⊤ =
    X.presheaf.map (homOfLE ⋯).op ≫
      X.presheaf.map (homOfLE ⋯).op ≫ (↑(↑U ⊓ ↑V)).presheaf.map (homOfLE H).op ≫ Hom.appLE F ⊤ ⊤ ⋯

Tactic:
simp only [homOfLE_leOfHom, Opens.toScheme_presheaf_map, Quiver.Hom.unop_op,
        Hom.opensFunctor_map_homOfLE, ← Functor.map_comp_assoc, IsAffineOpen.isoSpec_hom_appTop,
        Opens.topIso_inv, eqToHom_op, homOfLE_leOfHom, Category.assoc,
        Iso.inv_hom_id_assoc, F.app_eq_appLE]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
H : ⊤ ≤ X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE ⋯).op) ≫ Hom.appLE F ⊤ (F ⁻¹ᵁ ⊤) ⋯ =
    X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) ≫ Hom.appLE F ⊤ ⊤ ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯)) x = 0

Tactic:
have : (U.1.ι.app V.1 ≫ (I.glueDataObjι U).app (U.1.ι ⁻¹ᵁ V.1)).hom x = 0 :=
        I.ideal_le_ker_glueDataObjι U V hx

Goal state after:
case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
this : (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x = 0
⊢ (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯)) x = 0
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f✝¹ : X ⟶ Y
U✝ V : X.Opens
hU✝ : IsAffineOpen U✝
hV : IsAffineOpen V
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
f✝ : Spec R ⟶ X
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
⊢ x ∈ U

Tactic:
simpa using hU

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ ∀ f_1 ∈ (ker f).ideal ⟨U, hU⟩, f x ∉ Y.basicOpen f_1

Tactic:
intro s

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
s : ↑Γ(Y, U)
⊢ s ∈ (ker f).ideal ⟨U, hU⟩ → f x ∉ Y.basicOpen s
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
⊢ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U ≤ f.ker.ideal U

Tactic:
intro s

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
⊢ s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U → s ∈ f.ker.ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_1
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)
⊢ x ∈ (𝒰.X i).zeroLocus ↑((ker (Cover.pullbackHom 𝒰 f i)).ideal ⟨⊤, ⋯⟩)

Tactic:
· rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
        · exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩
        · exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2
        · exact (IsPullback.of_hasPullback _ _).flip

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun X ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x).1
h2 : (pullback.snd f g) z = (↑x).2
⊢ (↑((⇑(ConcreteCategory.hom (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) ∘
            ⇑(ConcreteCategory.hom (pullbackComparison forget f g)))
          z)).2 =
    (↑x).2

Tactic:
simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_snd]
    rwa [← types_comp_apply (g := pullback.snd _ _), pullbackComparison_comp_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (pullbackComparison (forgetToTop ⋙ CategoryTheory.forget TopCat) f g)

Tactic:
epi_iff_surjective

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (forgetToTop ⋙ CategoryTheory.forget TopCat) f g))
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget @IsImmersion

Tactic:
suffices IsZariskiLocalAtTarget
      (topologically fun {X Y} _ _ f ↦ IsLocallyClosed (Set.range f)) from
    isImmersion_eq_inf ▸ inferInstance

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget (topologically fun {X Y} x x_1 f ↦ IsLocallyClosed (Set.range f))
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: case e'_3
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
⊢ Set.range
      (comap
        ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
              C).comp
          (algebraMap R ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    (↑C).toSet

Tactic:
trans comap (Ideal.Quotient.mk I) '' (Set.range (comap (algebraMap _ (Localization.Away f))))

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 := ⋯
f : R ⧸ I := ⋯
⊢ Set.range
      (comap
        ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
              C).comp
          (algebraMap R ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    comap (Ideal.Quotient.mk I) '' Set.range (comap (algebraMap (R ⧸ I) (Localization.Away f)))

R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := ⋯
f : R ⧸ I := ⋯
⊢ comap (Ideal.Quotient.mk I) '' Set.range (comap (algebraMap (R ⧸ I) (Localization.Away f))) = (↑C).toSet
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X : Scheme
⊢ X.IsSeparated ↔ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
isSeparated_iff,

Goal state after:
X : Scheme
⊢ IsSeparated (terminal.from X) ↔ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case pos
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)

Tactic:
rw [Scheme.Cover.pullbackHom,
        ← (IsOpenImmersion.isPullback_lift_id _ _ hxU).flip.isoPullback_inv_snd,
        MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion]
      refine this (X.affineCover.f i ≫ f) _ ?_ ⟨_, rfl⟩
      rw [IsOpenImmersion.lift_fac_assoc, hg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
⊢ ∀ (f : ℕ →o Submodule R R), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
intro I

Goal state after:
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
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: 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)
⊢ ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s

Tactic:
intro s

Goal state after:
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)
s : ↥S
⊢ minN ↑s ∈ suitableN ↑s