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

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ Opens.IsBasis X.affineOpens

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ Opens.IsBasis (Set.range X.basicOpen)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
⊢ U.toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) = X.homOfLE h ≫ V.toSpecΓ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ U.toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) = U.ι ≫ X.toSpecΓ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ ⊤.toSpecΓ = ⊤.ι ≫ X.toSpecΓ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).toSpecΓ ≫ Spec.map (Hom.app f U) = f ∣_ U ≫ U.toSpecΓ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
hUV : V ≤ f ⁻¹ᵁ U
⊢ V.toSpecΓ ≫ Spec.map (Hom.appLE f U V hUV) = Hom.resLE f U V hUV ≫ U.toSpecΓ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ hU.isoSpec.hom x = (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsOpenImmersion hU.fromSpec

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.isoSpec.hom ≫ hU.fromSpec = U.ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)

Tactic:
by

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
f : R
⊢ Function.Surjective ⇑(toBasicOpenₗ R M f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑hU.fromSpec = ↑U

Tactic:
by

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
f : R
⊢ IsLocalizedModule.Away f (toOpenₗ R M (basicOpen f))

Tactic:
by

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
⊢ IsLocalizedModule ⊥ (toOpenₗ R M ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
⊢ (↑U).OpenCover

Tactic:
by

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
this : IsLocalizedModule ⊥ (toOpenₗ R M ⊤)
x y : M
e : (toOpenₗ R M ⊤) x = (toOpenₗ R M ⊤) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.fromSpec ≫ X.toSpecΓ = Spec.map (X.presheaf.map (homOfLE ⋯).op)

Tactic:
by

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
⊢ Function.Bijective ⇑(toOpenₗ R M ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = X.toRingedSpace.zeroLocus s

Tactic:
by

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 =
    toStalk R x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
i : J
x : F.obj { as := i }
⊢ (ConcreteCategory.hom (F.map (𝟙 { as := i }))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 { as := i }))) x = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
⊢ F.IsLocallyDirected

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: 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 : WidePushoutShape J
x : F.obj i
⊢ (ConcreteCategory.hom (F.map (𝟙 i))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 i))) x = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: 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))
j : J
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) x =
      (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) x ∧
    (ConcreteCategory.hom (F.map (𝟙 none))) x = x

Tactic:
by

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
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (RingHom.id R) r • (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: 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
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (𝟙 none))) x = x ∧
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) x =
      (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: 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
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (𝟙 none))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 none))) x = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: 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))
⊢ F.IsLocallyDirected

Tactic:
by

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
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Tactic:
by

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
⊢ equalizer.ι f g ≫ prod.lift f g = (equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)

Tactic:
by

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))
⊢ s.fst ≫ f = s.snd

Tactic:
by

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))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ g = s.snd

Tactic:
by

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))
⊢ equalizer.lift s.fst ⋯ ≫ equalizer.ι f g = s.fst

Tactic:
by

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))
⊢ equalizer.lift s.fst ⋯ ≫ equalizer.ι f g ≫ f = s.snd

Tactic:
by

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.lift s.fst ⋯

Tactic:
by

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
⊢ IsPullback (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))

Tactic:
by

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✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ coprod.desc f g ≫ coequalizer.π f g = coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g

Tactic:
by

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))
⊢ X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Tactic:
by

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✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = s.inr

Tactic:
by

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✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ g ≫ s.inl = s.inr

Tactic:
by

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✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ coequalizer.π f g ≫ coequalizer.desc s.inl ⋯ = s.inl

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f

Tactic:
by

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)
r : R
m : ↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x)
⊢ (Limits.colimit.isoColimitCocone
            {
              cocone :=
                (forget₂ (ModuleCat R) Ab).mapCocone
                  (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
              isColimit :=
                Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
                  (Limits.colimit.isColimit
                    ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }).addCommGroupIsoToAddEquiv.toFun
      (r • m) =
    (RingHom.id R) r •
      (Limits.colimit.isoColimitCocone
              {
                cocone :=
                  (forget₂ (ModuleCat R) Ab).mapCocone
                    (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
                isColimit :=
                  Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
                    (Limits.colimit.isColimit
                      ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }).addCommGroupIsoToAddEquiv.toFun
        m

Tactic:
by

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✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ (f ≫ coequalizer.π f g) ≫ coequalizer.desc s.inl ⋯ = s.inr

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ ⋯.fromSpec = X.isoSpec.inv

Tactic:
by

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)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • m = r • m

Tactic:
by

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✝¹ : 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
⊢ m = coequalizer.desc s.inl ⋯

Tactic:
by

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 = toStalkₗ' R M x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
⊢ IsUnit ((ConcreteCategory.hom (toStalk R x)) f)

Tactic:
by

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✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ IsPushout (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X)) (coequalizer.π f g) (f ≫ coequalizer.π f g)

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ s ≫ 𝟙 S = f ≫ t

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
⊢ toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 (Γ.obj (op X))

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.fst s v ≫ f = lhs ≫ pullback.fst t v

Tactic:
by

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)
f : R
hf : x ∈ basicOpen f
⊢ IsUnit ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
⊢ pullback.fst s v ≫ g = rhs ≫ pullback.fst t v

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ f = (equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ g

Tactic:
by

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
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Continuous ⇑hU.fromSpec

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ s = (equalizer.ι lhs rhs ≫ pullback.snd s v) ≫ v

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact ↑U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Set.range ⇑(U.ι ≫ f) = Set.range ⇑(f ''ᵁ U).ι

Tactic:
by

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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ s = (equalizer.ι lhs rhs ≫ pullback.snd s v) ≫ v

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (f ''ᵁ U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
by

Goal state after: