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

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy⟩

Tactic:
rw [PrimeSpectrum.basicOpen_mul] at hy

Goal state after:
case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy✝⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy✝⟩
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map i

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map i
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ ⋃ i, ↑↑i = ↑⊤

Tactic:
apply IsTopologicalBasis.sUnion_eq

Goal state after:
X : Scheme
⊢ IsTopologicalBasis (Set.range fun i ↦ ↑↑i)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    ((CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
          (CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (IsLocalization.map (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
                (CommRingCat.Hom.hom (Scheme.Hom.app f U)) ⋯)))).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))

Tactic:
RingHom.comp_assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
      ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (IsLocalization.map (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
                (CommRingCat.Hom.hom (Scheme.Hom.app f U)) ⋯))).comp
        (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R S : CommRingCat
⊢ Function.Surjective map

Tactic:
intro f

Goal state after:
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ ∃ a, map a = f
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
⊢ ∀ (x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl),
    IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)

Tactic:
by
      intro x
      have := IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
        (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ x, x.2⟩
      rw [Module.End.isUnit_iff] at this ⊢
      convert! this using 2 with a
      exact (IsScalarTower.algebraMap_smul ..).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst 0 0

Tactic:
simp [← Iso.eq_inv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.snd = pullback.snd 0 0

Tactic:
simp [← Iso.eq_inv_comp]

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)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
this : IsOpenImmersion α
⊢ α z = x

Tactic:
apply (pullback.fst (C := Scheme) _ _).isOpenEmbedding.injective

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)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι := ⋯
this : IsOpenImmersion α
⊢ (pullback.fst (V F i j).ι (V F i k).ι) (α z) = (pullback.fst (V F i j).ι (V F i k).ι) x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
⊢ (coprodSpec R S) x =
    (PrimeSpectrum.primeSpectrumProd R S).symm ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))).symm x)

Tactic:
by
  rw [← coprodSpec_coprodMk, Homeomorph.apply_symm_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
x : ↥(Spec (R ix))
y : ↥(Spec (R iy))
e :
  (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) ix))) x =
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) iy))) y
⊢ (DFinsupp.single iy 1) ix ∈ x.asIdeal

Tactic:
simp [h.symm]

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

Goal state before:
pp: case H
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
⊢ ∃ i, f x ∈ U i

Tactic:
exact ⟨x, h₁ x⟩

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

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y), P.toProperty f → P.toProperty (f ≫ e.hom)

Tactic:
rintro X Y Z e f ⟨a, h⟩; exact ⟨.of_isIso e.inv, h₂ e f h⟩

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

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
intro _ _ _ _ _ _; apply MorphismProperty.RespectsIso.precomp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: 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 := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsIso (Cover.pullbackHom (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i)

Tactic:
have : IsPullback (fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (fst _ _) := by
      simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _

Goal state after:
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 := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsIso (Cover.pullbackHom (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i)
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
⊢ colimit.ι F i =
    (F.mapIso (eqToIso ⋯)).hom ≫
      (Precoverage.ZeroHypercover.bind (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
            fun i ↦ (glueData F).openCover).f
        (((equivShrink J).trans (Equiv.uniqueSigma fun x ↦ Shrink.{u, w} J).symm) i)

Tactic:
by
  change colimit.ι F i = _ ≫ (glueData F).ι (equivShrink J i) ≫ _
  simp [← Category.assoc, ← Iso.comp_inv_eq, cocone]

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

Goal state before:
pp: case hP₂
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
⊢ closure[instTopologicalSpaceSubtype] {s.restrictPreimage f ⟨x, hx⟩} ⊆
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {⟨x, hx⟩}

Tactic:
⟨y, hy⟩

Goal state after:
case hP₂
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
⊢ ⟨y, hy⟩ ∈ closure[instTopologicalSpaceSubtype] {s.restrictPreimage f ⟨x, hx⟩} →
    ⟨y, hy⟩ ∈ s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {⟨x, hx⟩}
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₂
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : y ∈ closure[inst✝] {f x}
a : α
ha : a ∈ closure[inst✝¹] {x}
hay : f a = y
⊢ ⟨y, hy⟩ ∈ s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {⟨x, hx⟩}

Tactic:
rw [← specializes_iff_mem_closure] at hcl

Goal state after:
case hP₂
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : f x ⤳ y
a : α
ha : a ∈ closure[inst✝¹] {x}
hay : f a = y
⊢ ⟨y, hy⟩ ∈ s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {⟨x, hx⟩}
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
⊢ Q
    (this.isoPullback.hom ≫
      pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))

Tactic:
IsPullback.isoPullback_hom_snd

Goal state after:
Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
⊢ Q (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
erw [← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f)
      (AffineScheme.ofHom g)]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appTop
        ((PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)).inv ≫
          AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
⊢ SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks

Tactic:
by
  rw [eq_stalkwise, stalkwise_SpecMap_iff RingHom.surjective_respectsIso,
    RingHom.SurjectiveOnStalks]

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap e (f x) ≫ Scheme.Hom.stalkMap f x))

Tactic:
exact (RingHom.RespectsIso.cancel_left_isIso hP _ _).mpr <| hf x

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

Goal state before:
pp: case of_basicOpenCover
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
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
apply h₃ _ _ hs

Goal state after:
case of_basicOpenCover
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
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
⊢ ∀ (r : ↑↑s),
    (fun {R S} [CommRing R] [CommRing S] ↦ P)
      (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.FiniteHeight ↔ I = ⊤ ∨ I.height < ⊤

Tactic:
Ideal.finiteHeight_iff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I = ⊤ ∨ I.height ≠ ⊤ ↔ I = ⊤ ∨ I.height < ⊤
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal A
⊢ (under R J).height = J.height

Tactic:
rw [(J.comap _).height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal A
⊢ ⨅ J_1 ∈ (comap (algebraMap R A) J).minimalPrimes, J_1.height = ⨅ J_1 ∈ J.minimalPrimes, J_1.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
inst✝³ : I.IsPrime
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization.AtPrime A I
this : IsLocalRing A
⊢ ↑(under R (IsLocalRing.maximalIdeal A)).height = ↑I.height

Tactic:
← IsLocalization.AtPrime.under_maximalIdeal A I

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
inst✝³ : I.IsPrime
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization.AtPrime A I
this : IsLocalRing A
⊢ ↑(under R (IsLocalRing.maximalIdeal A)).height = ↑(under R (IsLocalRing.maximalIdeal A)).height
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁶ : IsZariskiLocalAtTarget P
inst✝⁵ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom ((algebraMap S T).comp f)))

Tactic:
have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization (S := T) r

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁶ : IsZariskiLocalAtTarget P
inst✝⁵ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom ((algebraMap S T).comp f)))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.f j)
i : Set.range ⇑(X.affineBasisCover.f j) ⊆ ↑U
U' : Opens ↥X := ⋯
i' : U' ⟶ U := ⋯
h₂' : P ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.f j))
⊢ P ⊤

Tactic:
apply h₃

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
⊢ ∀ (X : Scheme) (x : ↥X), P X x

Tactic:
intro X x

Goal state after:
P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
⊢ P X x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen f)

Tactic:
exact I.map_ideal_basicOpen _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
hx : (ConcreteCategory.hom (X.presheaf.map i.op)) x = 0
⊢ x = 0

Tactic:
rw [← basicOpen_eq_bot_iff] at hx ⊢

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
hx : X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) x) = ⊥
⊢ X.basicOpen x = ⊥
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫ (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom =
    (↑U).topIso.hom ≫ φ

Tactic:
simp only [Scheme.Hom.comp_app, TopologicalSpace.Opens.map_top, Category.assoc,
    Scheme.ΓSpecIso_naturality, Scheme.Opens.topIso_hom]

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.app (IsAffineOpen.isoSpec ⋯).inv ⊤ ≫ (ΓSpecIso Γ(X, ↑U)).hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ