mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R : TopCommRingCat
X : TopCommRingCat
x✝¹ : TopCatᵒᵖ
x✝ :
  ↑({ obj := fun X_1 ↦ continuousFunctions X_1 X, map := fun {x x_1} f ↦ continuousFunctions.pullback f X, map_id := ⋯,
          map_comp := ⋯ }.obj
      x✝¹)
⊢ (CommRingCat.Hom.hom ({ app := fun X_1 ↦ continuousFunctions.map X_1 (𝟙 X), naturality := ⋯ }.app x✝¹)) x✝ =
    (CommRingCat.Hom.hom
        ((𝟙
              { obj := fun X_1 ↦ continuousFunctions X_1 X, map := fun {x x_1} f ↦ continuousFunctions.pullback f X,
                map_id := ⋯, map_comp := ⋯ }).app
          x✝¹))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ ((opensFunctor U.ι).map (eqToHom ⋯)).op ≫ (homOfLE ⋯).op) =
    X.presheaf.map (𝟙 (op (⋯.functor.obj (X.homOfLE h ''ᵁ W))))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings ↑(⨆ i, U i)

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ (∀ (x : ↥↑(⨆ i, U i)), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)) ∧
    ∀ (i : { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.I₀),
      IsOpenImmersion ({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = U.ι

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ U)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ X.homOfLE i ≫ 𝟙 ↑(𝟙 X ⁻¹ᵁ V') = X.homOfLE i

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V ⋯)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
inst✝ : IsAffine X
e_2✝ : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
V : Opens ↥X
⊢ (∃ y, ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen y) = ↑V) ↔
    ∃ a,
      ↑{ carrier := ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen a),
            is_open' := ⋯ } =
        ↑V

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (eqToHom ⋯)) = (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ 𝟙 Γ(↑U, ⊤) = 𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ≫
      (structurePresheafInCommRingCat R).germ U x hxU =
    CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat R).map (homOfLE ⋯).op ≫ (structurePresheafInCommRingCat R).germ U x hxU

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map ((eqToHom ⋯).op ≫ f)) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
rfl

Goal state after:
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:
erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]

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) ≫
      X.presheaf.map ((X.toΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r)).leTop.op ≫ 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 : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • (modulePresheafStalkIso R M x).symm m =
    r • (modulePresheafStalkIso R M x).symm m

Tactic:
rfl

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
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx =
    (ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).map (homOfLE ⋯).op) ≫
      (structurePresheafInModuleCat R M).germ U x hx

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appTop hU.isoSpec.inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
IsAffineOpen.isoSpec_inv_appTop

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫
        (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ ((Scheme.Hom.opensFunctor U.ι).map (eqToHom ⋯).op.unop).op ≫ (eqToHom ⋯).op) ≫
      (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
rfl

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
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ openToLocalizationₗ R M ⊤ x _root_.trivial =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    f.c.app (op ⊤) ≫ ((pushforward CommRingCat f.base).obj X.presheaf).map (Y.toΓSpecMapBasicOpen r).leTop.op

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) = PrimeSpectrum.basicOpen f

Tactic:
← hU.fromSpec_preimage_basicOpen,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) = hU.fromSpec ⁻¹ᵁ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    (algebraMap ↑R ↑((structureSheaf ↑R).presheaf.stalk p)) x ∈
      IsLocalRing.maximalIdeal ↑((structureSheaf ↑R).presheaf.stalk p)

Tactic:
rfl

Goal state after:
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)
m : ↑(ModuleCat.of R M)
⊢ (ModuleCat.Hom.hom ((structurePresheafInModuleCat R M).germ ⊤ x _root_.trivial)) (const m 1 ⊤ ⋯) =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ ⊤ x ⋯)) (const m 1 ⊤ ⋯)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H :
  ∀ ⦃X Y : C⦄ ⦃f : X ⟶ Y⦄ ⦃R : Presieve Y⦄,
    R ∈ K.coverings Y → (P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], R g → P (pullback.snd f g))
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X} {U : C} {g : U ⟶ X},
    R ∈ K.coverings X → R g → P f → ∀ [inst : HasPullback f g], P (pullback.snd f g)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H :
  ∀ ⦃X Y : C⦄ ⦃f : X ⟶ Y⦄ ⦃R : Presieve Y⦄,
    R ∈ K.coverings Y → (P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], R g → P (pullback.snd f g))
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X},
    R ∈ K.coverings X → (∀ {U : C} {g : U ⟶ X} [inst : HasPullback f g], R g → P (pullback.snd f g)) → P f

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
R : CommRingCat
r : ↑(unop (op ((𝟭 CommRingCat).obj R)))
⊢ (SpecΓIdentity.inv.app R).op.unop ≫
      ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op =
    CommRingCat.ofHom
        (algebraMap (↑(unop (op ((𝟭 CommRingCat).obj R))))
          ((structureSheafInType ↑(unop (op ((𝟭 CommRingCat).obj R))) ↑(unop (op ((𝟭 CommRingCat).obj R)))).obj.obj
            (op (basicOpen r)))) ≫
      (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).c.app (op (basicOpen r))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} {f : X ⟶ Y} {R : Presieve X}, R ∈ K.coverings X → (P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f))
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
R✝ : Presieve X✝
hR : R✝ ∈ K.coverings X✝
x✝¹ : C
x✝ : x✝¹ ⟶ X✝
hg : R✝ x✝
hf : P f✝
⊢ P (x✝ ≫ f✝)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} {f : X ⟶ Y} {R : Presieve X}, R ∈ K.coverings X → (P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f))
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
R✝ : Presieve X✝
hR : R✝ ∈ K.coverings X✝
h : ∀ ⦃U : C⦄ ⦃g : U ⟶ X✝⦄, R✝ g → P (g ≫ f✝)
⊢ P f✝

Tactic:
grind

Goal state after:
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)ᵒᵖ
⊢ f.unop ≫
      ((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:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e_a
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)
r : R
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R R).presheaf.obj (op U))
this :
  germ (moduleStructurePresheaf R R).presheaf U x hxU ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ U x hxU)
⊢ (CommRingCat.Hom.hom ((structurePresheafInCommRingCat R).germ U x hxU))
      ((algebraMap R ((structureSheafInType R R).obj.obj (op U))) r) =
    (ConcreteCategory.hom ((structurePresheafInCommRingCat R).germ U x hxU))
      ((ConcreteCategory.hom ((structurePresheafInCommRingCat R).map (homOfLE ⋯).op))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) r))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
by
  rw [← Category.assoc, ← D.t_fac]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
by
  rw [← Category.assoc, ← D.t_fac]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R S : CommRingCat
φ ψ : R ⟶ S
⊢ Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ (ConcreteCategory.hom (Sigma.ι D.U i ≫ Multicoequalizer.sigmaπ D.diagram)) y =
    (ConcreteCategory.hom D.π)
      ((ConcreteCategory.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv) ⟨i, y⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ U.ι x = ↑x

Tactic:
rfl

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
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ LocalizedModule.mk (⟨σ ↑b, ⋯⟩ • f a) ⟨σ ↑b, ⋯⟩ = LocalizedModule.mk (σ ↑b • f a) ⟨σ ↑b, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_6
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
e_4✝ : ↑((Spec Γ(X, U)).presheaf.stalk y) = ↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)
e_5✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
⊢ (CommRingCat.Hom.hom ((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.germ ⊤ y ⋯)).toAlgebra =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U)) y)).toAlgebra

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = RingHom.id ↑((structureSheaf R).obj.obj (op U))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case none
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun x ↦
      Option.casesOn (motive := fun t ↦
        x = t →
          ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
        x (fun h ↦ ⋯ ▸ D.gluedIso F)
        (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
    ⋯
⊢ ((D.mapGlueData F).vPullbackCone i j).fst ≫ (D.mapGlueData F).ι i = F.map (D.f i j) ≫ (D.mapGlueData F).ι i

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case some.left
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun x ↦
      Option.casesOn (motive := fun t ↦
        x = t →
          ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
        x (fun h ↦ ⋯ ▸ D.gluedIso F)
        (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
    ⋯
⊢ ((D.mapGlueData F).vPullbackCone i j).π.app (some WalkingPair.left) = F.map (D.f i j)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case some.right
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun x ↦
      Option.casesOn (motive := fun t ↦
        x = t →
          ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
        x (fun h ↦ ⋯ ▸ D.gluedIso F)
        (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
    ⋯
⊢ ((D.mapGlueData F).vPullbackCone i j).π.app (some WalkingPair.right) = F.map (D.t i j) ≫ F.map (D.f j i)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⋃ i, ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i) = ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier

pp: case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⇑hU.fromSpec ⁻¹' U.carrier = Set.univ

Tactic:
· refine congr_arg (Set.iUnion ·) ?_
        ext1 x
        exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)

Goal state after:
case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⇑hU.fromSpec ⁻¹' U.carrier = Set.univ