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

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

Tactic:
constructor

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := ⋯
⊢ ∀
    (a :
      ↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x))),
    IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) a) → IsUnit a
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))

Tactic:
← TopCat.coe_comp,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base))
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:
constructor

Goal state after:
J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
⊢ ∀ {i j k : Discrete J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
    (ConcreteCategory.hom (F.map fi)) xi = (ConcreteCategory.hom (F.map fj)) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj
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:
constructor

Goal state after:
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 k : WidePushoutShape J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
    (ConcreteCategory.hom (F.map fi)) xi = (ConcreteCategory.hom (F.map fj)) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj
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 U

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 (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.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:
ext

Goal state after:
case h₁
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) ≫ prod.fst = ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) ≫ prod.fst

case h₂
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) ≫ prod.snd = ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) ≫ prod.snd
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:
ext

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
⊢ coprod.desc f g ≫ coequalizer.π f g = coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ coprod.inl ≫ coprod.desc f g ≫ coequalizer.π f g = coprod.inl ≫ coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g

case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ coprod.inr ≫ coprod.desc f g ≫ coequalizer.π f g = coprod.inr ≫ coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π 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
⊢ m = coequalizer.desc s.inl ⋯

Tactic:
ext

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 w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤)))
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (X.presheaf.Γgerm x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x)))
      (IsLocalRing.closedPoint ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) x)))

Tactic:
← IsLocalRing.comap_closedPoint (f.stalkMap x).hom,

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤)))
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (X.presheaf.Γgerm x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x)))
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Hom.stalkMap f x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))
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
⊢ pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs =
    pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs

Tactic:
ext

Goal state after:
case h₀
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 := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.fst t v =
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.fst t v

case h₁
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 := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.snd t v =
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.snd t v
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
⊢ pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
      equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
        ⋯ =
    𝟙 (equalizer lhs rhs)

Tactic:
ext

Goal state after:
case h₀
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 := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ ((pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
          equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯) ≫
        equalizer.ι lhs rhs) ≫
      pullback.fst s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.fst s v

case h₁
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 := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ ((pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
          equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯) ≫
        equalizer.ι lhs rhs) ≫
      pullback.snd s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.snd s v
Module: Mathlib.AlgebraicGeometry.StructureSheaf

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

Tactic:
ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
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
⊢ (equalizerPullbackMapIso hf hg v).hom ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v) =
    equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
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
⊢ ((equalizerPullbackMapIso hf hg v).hom ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫ pullback.fst s v =
    equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.fst s v

case h₁
C : Type u
inst✝² : Category.{v, u} C
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
⊢ ((equalizerPullbackMapIso hf hg v).hom ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫ pullback.snd s v =
    equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.snd s v
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) =
    (equalizerPullbackMapIso hf hg (𝒰.f i)).inv ≫
      equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
        (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ≫ pullback.fst s (𝒰.f i) =
    ((equalizerPullbackMapIso hf hg (𝒰.f i)).inv ≫
        equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
          (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)) ≫
      pullback.fst s (𝒰.f i)

case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ≫ pullback.snd s (𝒰.f i) =
    ((equalizerPullbackMapIso hf hg (𝒰.f i)).inv ≫
        equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
          (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)) ≫
      pullback.snd s (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e'_10
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)
e_5✝ : CommRing.toCommSemiring.toAddCommMonoid = inst✝⁴.toAddCommGroup.toAddCommMonoid
e_7✝ : Semiring.toModule ≍ Semiring.toModule
α : 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)) }
this :
  germ (moduleStructurePresheaf R R).presheaf ⊤ x ⋯ ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ ⊤ x ⋯)
⊢ Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x) =
    ↑(commRingCatStalkEquivModuleStalk R x) ∘ₗ toStalkₗ R R x

Tactic:
ext

Goal state after:
case e'_10
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)
e_5✝ : CommRing.toCommSemiring.toAddCommMonoid = inst✝⁴.toAddCommGroup.toAddCommMonoid
e_7✝ : Semiring.toModule ≍ Semiring.toModule
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) := ⋯
this :
  germ (moduleStructurePresheaf R R).presheaf ⊤ x ⋯ ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ ⊤ x ⋯)
⊢ (Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x)) 1 =
    (↑(commRingCatStalkEquivModuleStalk R x) ∘ₗ toStalkₗ R R x) 1
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ i y,
    (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) y =
      (ConcreteCategory.hom D.π) x'

Tactic:
rw [← dsimp% ConcreteCategory.congr_hom
    (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']

Goal state after:
D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ i y,
    (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) y =
      (ConcreteCategory.hom D.π)
        ((ConcreteCategory.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv)
          ((ConcreteCategory.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).hom) x'))
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
⊢ ⇑(hom π) ⁻¹' ⇑(hom π) '' U = U

Tactic:
ext

Goal state after:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U ↔ x✝ ∈ U
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U ↔ x✝ ∈ U

Tactic:
constructor

Goal state after:
case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U → x✝ ∈ U

case mpr
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ U → x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U
Module: Mathlib.Topology.Gluing

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

Tactic:
constructor

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y → D.Rel ⟨i, x⟩ ⟨j, y⟩

case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩ → (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case e
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ ↾⇑(ConcreteCategory.hom f.base) ≫ ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) =
    ↾⇑(ConcreteCategory.hom g.base) ≫ ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base)

Tactic:
ext

Goal state after:
case e
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
x✝ : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom
          (↾⇑(ConcreteCategory.hom f.base) ≫
            ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base))).toFun
      x✝ =
    (ConcreteCategory.hom
          (↾⇑(ConcreteCategory.hom g.base) ≫
            ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base))).toFun
      x✝