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

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CommRingCat.ofHom
            (algebraMap ↑(X.presheaf.obj (op ⊤))
              ↑((structureSheaf ↑(X.presheaf.obj (op ⊤))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.sheafedSpaceMap f).hom.base).obj U))) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
rw [Category.assoc]

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      (CommRingCat.ofHom
            (algebraMap ↑(X.presheaf.obj (op ⊤))
              ↑((structureSheaf ↑(X.presheaf.obj (op ⊤))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.sheafedSpaceMap f).hom.base).obj U))) ≫
        (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)
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
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.Hom.hom (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x) =
    ModuleCat.Hom.hom (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)))

Tactic:
refine IsLocalizedModule.ext x.asIdeal.primeCompl (LocalizedModule.mkLinearMap ..)
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap ..)) ?_

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.Hom.hom (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x) ∘ₗ
      LocalizedModule.mkLinearMap x.asIdeal.primeCompl M =
    ModuleCat.Hom.hom (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))) ∘ₗ
      LocalizedModule.mkLinearMap x.asIdeal.primeCompl M
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : K.HasPullbacks
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P f

Tactic:
by
  rw [IsLocalAtTarget.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
  simp [h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
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)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
let := Module.compHom N σ
  let := σ.toAlgebra
  have : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl
  apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
    (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ b, b.2⟩)).1
  dsimp
  rw [← (comapFun f y).map_smulₛₗ, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply]
  dsimp [comapFun, Localizations]
  refine (IsLocalizedModule.lift_apply ..).trans ?_
  dsimp
  rw [← LocalizedModule.mk_cancel ⟨σ b.1, b.2⟩, LocalizedModule.smul'_mk]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
⊢ f = g

Tactic:
by
  have : Mono φ := ConcreteCategory.mono_of_injective _ hφ
  rw [← IsOpenImmersion.lift_fac U.ι f (by simpa [Set.range_subset_iff] using fun x hx ↦ hUf.ge hx),
    ← IsOpenImmersion.lift_fac U.ι g (by simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx)]
  congr 1
  rw [← cancel_mono hU.isoSpec.hom, ← Spec.homEquiv.injective.eq_iff,
    ← cancel_mono φ, ← Spec.map_injective.eq_iff]
  simp [← cancel_mono U.ι, H]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_2
X : Scheme
inst✝ : IsAffine X
I : Ideal ↑Γ(X, ⊤)
⊢ IsClosed (X.zeroLocus ↑I)

Tactic:
exact zeroLocus_isClosed X I.carrier

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap g.hom x))

Tactic:
rw [PresheafedSpace.stalkMap.congr_hom _ _ (congr_arg InducedCategory.Hom.hom H.symm) x]

Goal state after:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (CommRingCat.Hom.hom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f.hom x))
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
⊢ (gluing 𝒰 f g).glued ⟶ X

Tactic:
by
  apply Multicoequalizer.desc (gluing 𝒰 f g).diagram _ fun i ↦ pullback.fst _ _ ≫ 𝒰.f i
  simp [t_fst_fst_assoc, ← pullback.condition]

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
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        invApp (D.f j i) ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))) ≫
          (D.U j).presheaf.map (eqToHom ⋯).op ≫ (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
rw [(D.f j k).c.naturality, f_invApp_f_app_assoc]

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

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun x ↦ Set.range ⇑(α (e.symm x))) i j

Tactic:
exact hα (fun h ↦ hij (e.symm.injective h))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
x : ↥X
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inl

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Goal state after:
X Y : Scheme
x : ↥X
⊢ colimit.ι (pair ↑X.toPresheafedSpace ↑Y.toPresheafedSpace) { as := WalkingPair.left } ≫
      (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inl
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
x : ↥Y
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inr

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Goal state after:
X Y : Scheme
x : ↥Y
⊢ colimit.ι (pair ↑X.toPresheafedSpace ↑Y.toPresheafedSpace) { as := WalkingPair.right } ≫
      (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inr
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_3
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ _root_.Pairwise (Function.onFun Disjoint fun x ↦ Scheme.Hom.opensRange (fi x))

Tactic:
· intro i j hij
    match i, j with
    | .left, .right => simpa [fi] using hf.1
    | .right, .left => simpa [fi] using hf.1.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Tactic:
have := Scheme.Hom.stalkMap_comp coprod.inr (coprodSpec R S) x

Goal state after:
case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this :
  Scheme.Hom.stalkMap (coprod.inr ≫ coprodSpec R S) x =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x) ≫ Scheme.Hom.stalkMap coprod.inr x
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))
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
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ R x) i)))

Tactic:
let := (Pi.evalRingHom R i).toAlgebra

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ R x) i)))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
⊢ IsAffineOpen (⨆ i, U ↑i)

Tactic:
have := hs.to_subtype

Goal state after:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
this : Finite ↑s
⊢ IsAffineOpen (⨆ i, U ↑i)
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) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)))

Tactic:
refine Function.Injective.comp ?_ (TopCat.GlueData.ι_injective D.toTopGlueData i)

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
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case mp
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f

Tactic:
⟨U, hU⟩

Goal state after:
case mp
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
U : Y.Opens
hU : U ∈ Y.affineOpens
⊢ AffineTargetMorphismProperty.of P (f ∣_ ↑⟨U, hU⟩)
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 : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : t F (↓i) ↓j ≫ (V F (↓j) ↓i).ι ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ F.map f ≫ (glueData F).ι j = (glueData F).ι i

Tactic:
simp only [t, IsOpenImmersion.lift_fac_assoc] at this

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 : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ F.map f ≫ (glueData F).ι j = (glueData F).ι 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
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact Multicoequalizer.π_desc _ _ _ _ _

Goal state after:
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
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.fst f f =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.snd f f

Tactic:
rw [← pullback.condition_assoc, ← pullback.condition_assoc]
        simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mpr
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)
⊢ (∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj) → (colimit.ι F i) xi = (colimit.ι F j) xj

Tactic:
rintro ⟨k, fi, fj, x, rfl, rfl⟩

Goal state after:
case mpr
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 : J
fi : k ⟶ i
fj : k ⟶ j
x : ↥(F.obj k)
⊢ (colimit.ι F i) ((F.map fi) x) = (colimit.ι F j) ((F.map fj) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

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

Tactic:
by
  constructor
  intro U hU hU'
  rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]
  apply QuasiCompact.isCompact_preimage
  · exact Continuous.isOpen_preimage (by fun_prop) _ hU
  apply QuasiCompact.isCompact_preimage <;> assumption

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

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
⊢ ∃ n, f ^ n * x = 0

Tactic:
have := hs.to_subtype

Goal state after:
case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : Finite ↑s
⊢ ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
U : ↑X.affineOpens
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
let S i : X.affineOpens := ⟨_, isAffineOpen_opensRange (𝒰.f i)⟩

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
U : ↑X.affineOpens
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
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 φ) ≫ (Scheme.ΓSpecIso S).hom)) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
Scheme.ΓSpecIso_naturality,

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 R).hom ≫ φ)) ↔ Q (CommRingCat.Hom.hom φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
this : ∀ {X : Scheme} (f : X ⟶ Y), P f → IsAffine X → P (f ≫ g)
hX : ¬IsAffine X
i : X.affineCover.I₀
⊢ P ((X.affineCover.f i ≫ f) ≫ g)

Tactic:
exact this _ (comp_of_isOpenImmersion _ _ _ hf) inferInstance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫ Y.residue ((ConcreteCategory.hom f.base) ↑x)) ≫
      CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫ X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ X.residue ↑x

Tactic:
rw [Category.assoc]

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
      Y.residue ((ConcreteCategory.hom f.base) ↑x) ≫
        CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫ X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ X.residue ↑x
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case refine_2
X Y : Scheme
f✝ : X ⟶ Y
U✝ V : X.Opens
hU : IsAffineOpen U✝
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
U : Opens ↥X
hxU : ⟨x, ⟨f, hf⟩⟩.fst ∈ U
⊢ X.presheaf.germ U ⟨x, ⟨f, hf⟩⟩.fst hxU ≫ ↑⟨x, ⟨f, hf⟩⟩.snd =
    X.presheaf.germ U ⟨x, ⟨f, hf⟩⟩.fst hxU ≫
      (X.presheaf.stalkCongr ⋯).hom ≫
        ↑((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
              ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).snd

Tactic:
simp only [Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk,
        TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ∀ (a : (MultispanShape.prod I.glueData.J).L),
    I.glueData.diagram.fst a ≫
        I.glueDataObjι ((MultispanShape.prod I.glueData.J).fst a) ≫ (↑((MultispanShape.prod I.glueData.J).fst a)).ι =
      I.glueData.diagram.snd a ≫
        I.glueDataObjι ((MultispanShape.prod I.glueData.J).snd a) ≫ (↑((MultispanShape.prod I.glueData.J).snd a)).ι

Tactic:
simp [GlueData.diagram, pullback.condition_assoc]

Goal state after: