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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op))
          (const (∑ i, c i • a i) (↑⟨f ^ (n + 1), ⋯⟩) (basicOpen f) ⋯))
      x =
    ↑(const (a i) (b i) (basicOpen (b i)) ⋯) x

Tactic:
refine LocalizedModule.mk_eq.mpr ⟨1, ?_⟩

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ 1 • ⟨b i, ⋯⟩ • ∑ i, c i • a i = 1 • ⟨↑⟨f ^ (n + 1), ⋯⟩, ⋯⟩ • a i
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ Scheme.Hom.appTop hU.isoSpec.hom

Tactic:
isoSpec_hom_appTop

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of ↑(unop (op (CommRingCat.of R)))))).unop ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app (op ⊤) ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
simp_rw [← Γ_map_op]

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      Γ.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).op ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comap (RingHom.id R) U V ⋯) s) p = ↑((CommRingCat.Hom.hom ((structureSheaf R).obj.map iVU.op)) s) p

Tactic:
comap_apply

Goal state after:
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (RingHom.id R) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨PrimeSpectrum.comap (RingHom.id R) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).obj.map iVU.op)) s) p
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
x✝ : ↑(CommRingCat.of R)
x : ↥(unop (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))
⊢ ↑((comap f U ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)
          ((algebraMap R ↑((structureSheaf R).obj.obj (op U))) x✝))
      x =
    ↑((algebraMap S
            ↑((structureSheaf S).obj.obj
                (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))
          (f x✝))
      x

Tactic:
comap_apply

Goal state after:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
x✝ : ↑(CommRingCat.of R)
x : ↥(unop (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑x).asIdeal (↑x).asIdeal f ⋯)
      (↑((algebraMap R ↑((structureSheaf R).obj.obj (op U))) x✝) ⟨PrimeSpectrum.comap f ↑x, ⋯⟩) =
    ↑((algebraMap S
            ↑((structureSheaf S).obj.obj
                (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))
          (f x✝))
      x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image,
      Set.iUnion_exists, Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res,
      Opens.coe_inf, Opens.coe_mk, Set.iUnion_subset_iff]

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ∀ i ∈ s, ↑V ∩ ↑(X.basicOpen i) ⊆ ⋃ i ∈ s, ↑(X.basicOpen i)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit
    (Cofork.ofπ
      (InducedCategory.homMk
        (homMk
            (coequalizer.π (Hom.toShHom (F.map WalkingParallelPairHom.left))
              (Hom.toShHom (F.map WalkingParallelPairHom.right)))
            ⋯).toHom)
      ⋯)

Tactic:
exact coequalizerIsCoequalizer _ _

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (((pullback.snd (D.f i j) (D.f i k)).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
          (D.t' k i j).c.app
            (op
              ((Opens.map (pullback.snd (D.f i j) (D.f i k)).base).obj
                ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)))) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U)

Tactic:
rw [← comp_c_app, congr_app (D.t_fac k i j), comp_c_app]

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    ((((D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
            (pullback.fst (D.f k i) (D.f k j)).c.app
              (op
                ((Opens.map (D.t k i).base).obj
                  (unop (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)))))) ≫
          (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
⊢ X ⟶ Y

Tactic:
by
  refine inv 𝒰.ulift.fromGlued ≫ ?_
  fapply Multicoequalizer.desc
  · exact fun i ↦ f _
  rintro ⟨i, j⟩
  dsimp
  change pullback.fst _ _ ≫ f _ = (_ ≫ _) ≫ f _
  simpa [pullbackSymmetry_hom_comp_fst] using hf _ _

Goal state after:
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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
y₁ : ↥(F.obj k₁.fst)
hy₁ : (F.map k₁.snd.1) y₁ = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x

Tactic:
obtain ⟨k₂, y₂, hy₂⟩ := mem_iSup.mp ((pullback.snd (C := Scheme) _ _) x).2

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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
y₁ : ↥(F.obj k₁.fst)
hy₁ : (F.map k₁.snd.1) y₁ = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
y₂ : ↥(F.obj k₂.fst)
hy₂ : (F.map k₂.snd.1) y₂ = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv)

Tactic:
rw [← TopCat.mono_iff_injective]

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono (D.gluedIso (forget C)).inv
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ⇑(ConcreteCategory.hom (D.f j k ≫ D.ι j).base) ⁻¹' ↑(⋯.functor.obj U) =
    ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.left (j, k))).base) ⁻¹' ↑(⋯.functor.obj U)

Tactic:
congr 4

Goal state after:
case left.e_f
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ D.f j k ≫ D.ι j = colimit.ι D.diagram.multispan (WalkingMultispan.left (j, k))
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
by
  rw [mono_iff_injective]
  cases i
  · simpa using! f.isOpenEmbedding.injective
  · simpa using! g.isOpenEmbedding.injective

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.toPreZeroHypercover.1), P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ ∀ (i : 𝒰.I₀), P (f ∣_ Scheme.Hom.opensRange (𝒰.f i))

Tactic:
exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (H i)

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

Goal state before:
pp: case hf
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : ↥X → Y.Opens
h₁ : ∀ (x : ↥X), f x ∈ U x
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
x : ↥X
⊢ P (f ∣_ U x)

Tactic:
exact P.of_postcomp (f ∣_ U x) (U x).ι (inferInstance : IsOpenImmersion _) (by simp [h₂])

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit))

Tactic:
convert! hg

Goal state after:
case e'_3
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
e_2✝ : (coprodOpenCover X' Y').X (Sum.inr PUnit.unit) = Y'
⊢ ⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit) = g
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case inj
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
this : (D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv = (D.ι i).base
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv)

Tactic:
rw [← TopCat.mono_iff_injective]

Goal state after:
case inj
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
this : (D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv = (D.ι i).base
⊢ Mono (D.gluedIso (forget C)).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ x ∈ ⨆ x, V x

Tactic:
simp only [Opens.mem_iSup]

Goal state after:
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ ∃ i, x ∈ V i
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ P.toProperty f ↔ P f

Tactic:
delta AffineTargetMorphismProperty.toProperty

Goal state after:
P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ (∃ (h : IsAffine Y), P f) ↔ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: ⊢ IsStableUnderBaseChange @IsPreimmersion

Tactic:
by
  refine .mk' fun X Y Z f g _ _ ↦ ?_
  have := pullback_fst (P := @SurjectiveOnStalks) f g inferInstance
  constructor
  let L (x : (pullback f g :)) : { x : X × Y | f x.1 = g x.2 } :=
    ⟨⟨pullback.fst f g x, pullback.snd f g x⟩,
    by simp only [Set.mem_ofPred, ← Scheme.Hom.comp_apply, pullback.condition]⟩
  have : IsEmbedding L := IsEmbedding.of_comp (by fun_prop) continuous_subtype_val
    (SurjectiveOnStalks.isEmbedding_pullback f g)
  exact IsEmbedding.subtypeVal.comp ((TopCat.pullbackHomeoPreimage _ f.continuous _
    g.isEmbedding).isEmbedding.comp this)

Goal state after:
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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,

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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ Q ((CommRingCat.Hom.hom (Scheme.ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ)))) ↔
    Q (CommRingCat.Hom.hom φ)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.refine_2.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ (RelSeries.last p).asIdeal.height ≤ ⨆ (_ : (RelSeries.last p).asIdeal ≠ ⊤), (RelSeries.last p).asIdeal.height

Tactic:
exact le_iSup_of_le p.last.isPrime.ne_top' le_rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
⊢ _root_.IsReduced ↑(X.presheaf.stalk x)

Tactic:
constructor
  rintro g ⟨n, e⟩
  obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.exists_germ_eq g
  rw [← map_pow, ← map_zero (X.presheaf.germ _ x hxU).hom] at e
  obtain ⟨V, hxV, iU, iV, (e' : (X.presheaf.map iU.op) (s ^ n) = (X.presheaf.map iV.op) 0)⟩ :=
    X.presheaf.germ_eq x hxU hxU _ 0 e
  rw [map_pow, map_zero] at e'
  replace e' := (IsNilpotent.mk _ _ e').eq_zero (R := Γ(X, V))
  rw [← X.presheaf.germ_res iU x hxV, CommRingCat.comp_apply, e', map_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: R : CommRingCat
⊢ IsReduced (Spec R) ↔ _root_.IsReduced ↑R

Tactic:
refine ⟨?_, fun h => inferInstance⟩
  intro h
  exact isReduced_of_injective (Scheme.ΓSpecIso R).inv.hom
    (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv.injective

Goal state after:
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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
hYa : ∃ a, U = Y.basicOpen a
⊢ P (f ≫ U.ι)

Tactic:
obtain ⟨a, rfl⟩ := hYa

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
⊢ P (f ≫ (Y.basicOpen a).ι)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
⊢ False

Tactic:
have : Nonempty (⟨Sᶜ, hS.1⟩ ⊔ ⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, Or.inl h₂.choose_spec⟩⟩

Goal state after:
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
⊢ False
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 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)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
      intro U
      rw [morphismRestrict_comp]
      exact this _ inferInstance _ (IsZariskiLocalAtTarget.restrict hf _) U.2

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

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↥X
⊢ ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
obtain ⟨U, V, hxV, e, hf⟩ := hf x
    use U, V, hxV, e
    simp only [iff_of_isAffine (P := P), Scheme.Hom.appLE, homOfLE_leOfHom] at hf ⊢
    have : (toMorphismProperty (Locally Q)).RespectsIso := toMorphismProperty_respectsIso_iff.mp <|
      (isLocal_ringHomProperty P).respectsIso
    exact (MorphismProperty.arrow_mk_iso_iff (toMorphismProperty (Locally Q))
      (arrowResLEAppIso f U V e)).mpr (locally_of hQi _ hf)

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

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝¹ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this✝ : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f ↑Γ(X, ↑U)
⊢ RingHom.ker (Ideal.Quotient.mk (I.ideal U)) ≤
    Ideal.map (algebraMap ↑Γ(X, ↑V) ↑Γ(X, ↑U)) (RingHom.ker (Ideal.Quotient.mk (I.ideal V)))

Tactic:
· simp only [Ideal.mk_ker, RingHom.algebraMap_toAlgebra, I.map_ideal', le_refl]

Goal state after: