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

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f.liftQuotient I hI ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X ⟶ Spec A
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (specTargetImageFactorization f)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R : CommRingCat
x : PrimeSpectrum ↑R
⊢ CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R : CommRingCat
x : PrimeSpectrum ↑R
⊢ (Spec R).presheaf.germ ⊤ x trivial ≫ (stalkIso R x).hom =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R✝ S✝ : CommRingCat
f✝ : R✝ ⟶ S✝
p✝ : PrimeSpectrum ↑S✝
x : PrimeSpectrum ↑R✝
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
      (Arrow.mk
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk (Hom.stalkMap (Spec.map f) p)).hom ≫ (Spec.stalkIso S p).hom

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t i j ≫ D.f j i)) '' ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
U : Opens ↑(D.U i)
⊢ IsOpen (⇑(ConcreteCategory.hom (D.ι i)) '' ↑U)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j : h.J
⊢ IsIso (h.t i j)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶ pullback (h.V j k).inclusion' (h.V j i).inclusion'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i : h.J
⊢ h.t i i = 𝟙 ((Opens.toTopCat (h.U (i, i).1)).obj (h.V (i, i).1 (i, i).2))

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ h.t' i j k ≫ pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
⊢ IsLocalRing ↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk x)

Tactic:
by

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

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
⊢ Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
y : ↑↑Y.toPresheafedSpace
h : ↑(s.pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.desc (Hom.toShHom s.π) e).hom.base)
        ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))) →+*
  ↑((coequalizerCofork f g).pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y)) :=
  CommRingCat.Hom.hom
    (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))
x✝ : IsLocalHom ((CommRingCat.Hom.hom ((coequalizerCofork f g).π.stalkMap y)).comp h)
⊢ IsLocalHom h

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ h.t' i j k ≫ h.t' j k i ≫ h.t' k i j = 𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion')

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i j : J
⊢ Continuous fun x ↦ ⟨⟨↑↑x, ⋯⟩, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
⊢ (Opens.map (U i).inclusion').obj (U i) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
⊢ ⇑(ConcreteCategory.hom (ofHom { toFun := fun x ↦ ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ })) = id

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
⊢ IsColimit (coequalizerCofork f g)

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit F forgetToSheafedSpace

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ ∀ (a : (MultispanShape.prod (ofOpenSubsets U).J).L),
    (ofOpenSubsets U).diagram.fst a ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).fst a)).inclusion' =
      (ofOpenSubsets U).diagram.snd a ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).snd a)).inclusion'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
Y : Over X
m : Y ⟶ mk (𝟙 X)
⊢ Hom.left m = Hom.left (homMk Y.hom ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T : Over X
f : S ⟶ T
⊢ R.hom ≫ 𝟙 X = 𝟙 R.left ≫ R.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T : Over X
f : S ⟶ T
⊢ S.hom ≫ 𝟙 X = Hom.left f ≫ T.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T U : Over X
f : R ⟶ S
g : T ⟶ U
⊢ R.hom ≫ 𝟙 X = Hom.left f ≫ S.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T U : Over X
f : R ⟶ S
g : T ⟶ U
⊢ T.hom ≫ 𝟙 X = Hom.left g ≫ U.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R : C
f : R ⟶ X
⊢ Hom.left (LaxMonoidal.ε (pullback f)) = inv (pullback.snd (𝟙 X) f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (LaxMonoidal.μ (pullback f) R S) ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Function.Injective ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (LaxMonoidal.μ (pullback f) R S) ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.snd R.hom S.hom =
    pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.hom f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (LaxMonoidal.μ (pullback f) R S) ≫ pullback.snd (R ⊗ S).hom f =
    pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B R S Y Z : C
f✝ : R ⟶ X
g : S ⟶ X
f : R ⟶ S
⊢ (asIso (pullback.snd (𝟙 S) f)).hom ≫ (𝟙_ (Over R)).hom = ((pullback f).obj (𝟙_ (Over S))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
R S : C
f : R ⟶ S
⊢ preservesTerminalIso (pullback f) = isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.f i j)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ SheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.f i j)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ PresheafedSpace.IsOpenImmersion
    (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i j)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
A B : Over Y
⊢ Hom.left (prodComparisonIso (pullback f) A B).inv ≫
      pullback.fst (pullback.fst A.hom B.hom ≫ A.hom) f ≫ pullback.fst A.hom B.hom =
    pullback.fst (pullback.snd A.hom f) (pullback.snd B.hom f) ≫ pullback.fst A.hom f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫
      pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd gA gB =
    pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.fst (mk gB).hom f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (D.ι i).base)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫ pullback.snd (pullback.fst gA gB ≫ gA) f =
    pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ IsOpenMap ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst✝ : MonObj (mk f)
⊢ pullback.snd f (𝟙 X) ≫ 𝟙 X = (mk (pullback.snd f (𝟙 X))).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ Scheme

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ IsOpenImmersion (D.ι i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ D.f i j ≫ D.ι i = (D.t i j ≫ D.f j i) ≫ D.ι j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ ↑D.glued.toPresheafedSpace ≅
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) = ⋃ i, ↑(U i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst✝ : MonObj (mk f)
⊢ MonObj.mul ≫ homMk (pullback.fst f (𝟙 X)) ⋯ =
    (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ MonObj.mul

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan 0 X), s.snd ≫ 0 = s.fst

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan 0 X), s.snd ≫ 𝟙 X = s.snd

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryFan 0 X
m : s.pt ⟶ X
x✝ : m ≫ 0 = s.fst
h₂ : m ≫ 𝟙 X = s.snd
⊢ m = s.snd

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (zeroProdIso X).inv ≫ prod.snd = 𝟙 X

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan X 0), s.fst ≫ 𝟙 X = s.fst

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan X 0), s.fst ≫ 0 = s.snd

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryFan X 0
m : s.pt ⟶ X
h₁ : m ≫ 𝟙 X = s.fst
x✝ : m ≫ 0 = s.snd
⊢ m = s.fst

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (prodZeroIso X).inv ≫ prod.fst = 𝟙 X

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan 0 X), 0 ≫ s.inr = s.inl

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan 0 X), 𝟙 X ≫ s.inr = s.inr

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryCofan 0 X
m : X ⟶ s.pt
x✝ : 0 ≫ m = s.inl
h₂ : 𝟙 X ≫ m = s.inr
⊢ m = s.inr

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan X 0), 𝟙 X ≫ s.inl = s.inl

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan X 0), 0 ≫ s.inl = s.inr

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryCofan X 0
m : X ⟶ s.pt
h₁ : 𝟙 X ≫ m = s.inl
x✝ : 0 ≫ m = s.inr
⊢ m = s.inl

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inl

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫ D.isoCarrier.inv =
    (D.ι i).base

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl 0 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr 0 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
⊢ ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) ''
      ⇑(ConcreteCategory.hom (pullback.fst (D.f i j) (D.f i k)).base) ⁻¹' S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
⊢ op
      ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj
        (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U)))))) =
    (Opens.map (D.f i k).base).op.obj (op ((opensFunctor (D.f i j)).obj U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
U : Set ↥D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i) ⁻¹' U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D✝ : GlueData
D : GlueData
⊢ { I₀ := D.J, X := D.U, f := D.ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings D.glued

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case refine_1
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) ≫ 𝟙 X =
    (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom ≫ pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case refine_1
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) ≫ 𝟙 X =
    (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom ≫ pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y

pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ 𝒰.f z ≫ 𝟙 X = 𝟙 (𝒰.X z) ≫ 𝒰.f z

Tactic:
· simp [pullback.condition]

Goal state after:
case refine_2
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ 𝒰.f z ≫ 𝟙 X = 𝟙 (𝒰.X z) ≫ 𝒰.f z