mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V' ⋯)
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:
;

Goal state after:
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 ⋯)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x ∈ ⊤

Tactic:
;

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
i : (Scheme.coverOfIsIso (𝟙 X)).I₀
⊢ IsAffine X

Tactic:
;

Goal state after:
X : Scheme
inst✝ : IsAffine X
i : (Scheme.coverOfIsIso (𝟙 X)).I₀
⊢ IsAffine X
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
apply Opens.ext

Goal state after:
X : Scheme
⊢ ↑(⨆ i, ↑i) = ↑⊤
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:
;

Goal state after:
X : Scheme
⊢ (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (eqToHom ⋯)) = (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(hU.isoSpec.inv ≫ U.ι) = ↑U

Tactic:
;

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(hU.isoSpec.inv ≫ U.ι) = ↑U
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),
    let U := basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
          (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.c.app (op 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:
intro r

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
⊢ let U := basicOpen r;
  (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
        (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.c.app (op 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.CategoryTheory.LocallyDirected

Goal state before:
pp: case init.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

Tactic:
· simp only [((CategoryTheory.mono_iff_injective (F.map (.init i))).mp inferInstance).eq_iff,
      forall_eq']
    exact fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
x✝ : m ≫ equalizer.ι f g ≫ f = s.snd
⊢ m ≫ equalizer.ι f g = equalizer.lift s.fst ⋯ ≫ equalizer.ι f g

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
x✝ : m ≫ equalizer.ι f g ≫ f = s.snd
⊢ m ≫ equalizer.ι f g = equalizer.lift s.fst ⋯ ≫ equalizer.ι f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
x✝ : (f ≫ coequalizer.π f g) ≫ m = s.inr
⊢ coequalizer.π f g ≫ m = coequalizer.π f g ≫ coequalizer.desc s.inl ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
x✝ : (f ≫ coequalizer.π f g) ≫ m = s.inr
⊢ coequalizer.π f g ≫ m = coequalizer.π f g ≫ coequalizer.desc s.inl ⋯
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 =
      CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).c.app (op (basicOpen r))

Tactic:
intro r

Goal state after:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    CommRingCat.ofHom
        (algebraMap (↑(unop (Γ.rightOp.obj Y)))
          ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
      ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).c.app (op (basicOpen r))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U = (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
rw [← hU.ΓSpecIso_hom_fromSpec_app, Iso.inv_hom_id_assoc]

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:
;

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen r ⊓ U)

Tactic:
inf_comm,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (U ⊓ X.basicOpen r)
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:
intro r

Goal state after:
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))
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.IsLocalAtTarget K
X Y✝ : C
f : X ⟶ Y✝
𝒰 : K.ZeroHypercover Y✝
inst✝¹ : K.HasPullbacks
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
Y : C
i : 𝒰.I₀
inst✝ : HasPullback f (𝒰.f i)
⊢ P (pullback.snd f (𝒰.f i))

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : P.IsLocalAtTarget K
X Y✝ : C
f : X ⟶ Y✝
𝒰 : K.ZeroHypercover Y✝
inst✝¹ : K.HasPullbacks
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
Y : C
i : 𝒰.I₀
inst✝ : HasPullback f (𝒰.f i)
⊢ P (pullback.snd f (𝒰.f i))
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:
;

Goal state after:
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))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ identityToΓSpec.app (Spec.toLocallyRingedSpace.obj R) ≫
      Spec.toLocallyRingedSpace.map ((NatIso.op SpecΓIdentity).inv.app R) =
    𝟙 (Spec.toLocallyRingedSpace.obj R)

Tactic:
simp only [Functor.id_obj, NatIso.op_inv, NatTrans.op_app, SpecΓIdentity_inv_app]
    exact right_triangle R.unop

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.IsLocalAtSource K
X Y✝ : C
f : X ⟶ Y✝
𝒰 : K.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Y : C
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtSource K
X Y✝ : C
f : X ⟶ Y✝
𝒰 : K.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Y : C
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
;

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
x : X
⊢ (hom (f ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g))).toFun x =
    (hom (g ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g))).toFun x

Tactic:
;

Goal state after:
X Y Z : Type u
f g : X ⟶ Y
x : X
⊢ (hom (f ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g))).toFun x =
    (hom (g ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g))).toFun x
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
x : (fun X ↦ X) X
⊢ (⇑(hom s.π) ∘ ⇑(hom f)) x = (⇑(hom s.π) ∘ ⇑(hom g)) x

Tactic:
;

Goal state after:
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
x : (fun X ↦ X) X
⊢ (⇑(hom s.π) ∘ ⇑(hom f)) x = (⇑(hom s.π) ∘ ⇑(hom g)) x
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
x✝¹ : Cofork f g
x✝ : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt ⟶ x✝¹.pt
hm : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).π ≫ x✝ = x✝¹.π
x : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt
⊢ (hom x✝).toFun x = (hom (↾Function.Coequalizer.desc ⇑(hom f) ⇑(hom g) ⇑(hom x✝¹.π) ⋯)).toFun x

Tactic:
;

Goal state after:
X Y Z : Type u
f g : X ⟶ Y
x✝¹ : Cofork f g
x✝ : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt ⟶ x✝¹.pt
hm : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).π ≫ x✝ = x✝¹.π
x : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt
⊢ (hom x✝).toFun x = (hom (↾Function.Coequalizer.desc ⇑(hom f) ⇑(hom g) ⇑(hom x✝¹.π) ⋯)).toFun x
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
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s t : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩ + ↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) =
    (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) +
      (Localizations.comapFun f ↑x✝) (↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩)

Tactic:
;

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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s t : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩ + ↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) =
    (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) +
      (Localizations.comapFun f ↑x✝) (↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩)
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
⊢ ((asIso (Scheme.Hom.stalkMap hU.fromSpec y)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec y)))).toAlgebra =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U)) y)).toAlgebra

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, IsAffineOpen.fromSpec_app_self]

Goal state after:
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
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: 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)
⊢ IsLimit (F.mapCone (D.vPullbackCone i j))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm _

Goal state after:
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)
⊢ IsLimit (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: 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)
x : WalkingCospan
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅ (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x

Tactic:
by
        cases x
        exacts [D.gluedIso F, Iso.refl _]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

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

Tactic:
rw [comap_id rfl]

Goal state after:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = RingHom.id ↑((structureSheaf R).obj.obj (op U))
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:
;

Goal state after:
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
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:
;

Goal state after:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = RingHom.id ↑((structureSheaf R).obj.obj (op U))
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:
;

Goal state after:
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)