mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      limit.π
          ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                  U)))
          (op j) ≫
        (F.obj j).presheaf.map (eqToHom ⋯) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
limMap_π_assoc

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limit.π (componentwiseDiagram F U) (op j) ≫
      (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫
        (F.obj j).presheaf.map (eqToHom ⋯) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1.refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ ↑(unop (op W)) ⟶ ↑(unop U)

pp: case refine_1.refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩ ∧
    (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩

Tactic:
·

Goal state after:
case refine_1.refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ ↑(unop (op W)) ⟶ ↑(unop U)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1.refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩ ∧
    (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩

Tactic:
·

Goal state after:
case refine_1.refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩ ∧
    (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case w
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.base = (𝟙 (sheafedSpaceObj R)).hom.base

pp: case h
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (𝟙 (sheafedSpaceObj R)).hom.c

Tactic:
·

Goal state after:
case w
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.base = (𝟙 (sheafedSpaceObj R)).hom.base
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (𝟙 (sheafedSpaceObj R)).hom.c

Tactic:
·

Goal state after:
case h
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (𝟙 (sheafedSpaceObj R)).hom.c
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base

pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c

Tactic:
·

Goal state after:
case w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c

Tactic:
·

Goal state after:
case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.base = β.hom.base

pp: case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c

Tactic:
·

Goal state after:
case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.base = β.hom.base
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c

Tactic:
·

Goal state after:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case app
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (X_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ) →
    (Y.restrict ⋯).presheaf.obj X_1 ≅ ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).obj X_1

pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ autoParam
    (∀ {X_1 Y_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
      (Y.restrict ⋯).presheaf.map f_1 ≫ Iso.hom (?app Y_1) =
        Iso.hom (?app X_1) ≫ ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1)
    NatIso.ofComponents._auto_1

Tactic:
·

Goal state after:
case app
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (X_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ) →
    (Y.restrict ⋯).presheaf.obj X_1 ≅ ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).obj X_1
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ autoParam
    (∀ {X_1 Y_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
      (Y.restrict ⋯).presheaf.map f_1 ≫
          (asIso (f.c.app (op ((opensFunctor f).obj (unop Y_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
        (asIso (f.c.app (op ((opensFunctor f).obj (unop X_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
          ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1)
    NatIso.ofComponents._auto_1

Tactic:
·

Goal state after:
case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ autoParam
    (∀ {X_1 Y_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
      (Y.restrict ⋯).presheaf.map f_1 ≫
          (asIso (f.c.app (op ((opensFunctor f).obj (unop Y_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
        (asIso (f.c.app (op ((opensFunctor f).obj (unop X_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
          ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1)
    NatIso.ofComponents._auto_1
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f

Tactic:
refine PresheafedSpace.Hom.ext _ _ rfl <| NatTrans.ext <| funext fun x => ?_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ (((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app x = f.c.app x
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case inl
X : Scheme
b : ↥X
hx : IsClosed {b}
a✝ : b ≤ b
⊢ b ≤ b

pp: case inr
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
a✝ : b ≤ x
h : b ≠ x
⊢ x ≤ b

Tactic:
·

Goal state after:
case inl
X : Scheme
b : ↥X
hx : IsClosed {b}
a✝ : b ≤ b
⊢ b ≤ b
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case inr
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
a✝ : b ≤ x
h : b ≠ x
⊢ x ≤ b

Tactic:
·

Goal state after:
case inr
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
a✝ : b ≤ x
h : b ≠ x
⊢ x ≤ b
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) =
    f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x))

pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x

Tactic:
·

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) =
    f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x

Tactic:
·

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (g.c.app (op (h.functor.obj U)))

pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))

Tactic:
·

Goal state after:
case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (g.c.app (op (h.functor.obj U)))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk.mk.w
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.base = toLRSHom'✝.base

pp: case h
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c

Tactic:
·

Goal state after:
case mk.mk.w
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.base = toLRSHom'✝.base
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))

Tactic:
·

Goal state after:
case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case h
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c

Tactic:
·

Goal state after:
case h
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
⊢ appLE (f ≫ g) U V e = appLE g U (g ⁻¹ᵁ U) ⋯ ≫ appLE f (g ⁻¹ᵁ U) V e

Tactic:
appLE_comp_appLE

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
⊢ appLE (f ≫ g) U V e = appLE (f ≫ g) U V ⋯
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_4
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))

pp: case e'_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op ≍ Y.presheaf.map (𝟙 (op (hf.functor.obj U)))

pp: case convert_2
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))

Tactic:
·

Goal state after:
case e'_4
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op ≍ Y.presheaf.map (𝟙 (op (hf.functor.obj U)))

pp: case convert_2
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))

Tactic:
·

Goal state after:
case e'_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op ≍ Y.presheaf.map (𝟙 (op (hf.functor.obj U)))