awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)
⊢ Subset (α := Set (↑(D.mapGlueData (forget C)).glued : Type v))
    (Set.image (α := (↑(↑(D.U j) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) (D.toTopGlueData.ι j)) :
        (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))
      (Set.image (α := (↑(↑s.pt : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              s.snd.base) :
          (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
        Set.univ))
    (Set.range (ι := (↑(↑(D.U j) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι j)) :
        (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))

Tactic:
Set.image_subset_range _ _

Premises used: Set.image_subset_range, CategoryTheory.GlueData.mapGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)
⊢ Subset (α := Set (↑(D.mapGlueData (forget C)).glued : Type v))
    (Set.image (α := (↑(↑(D.U j) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) (D.toTopGlueData.ι j)) :
        (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))
      (Set.image (α := (↑(↑s.pt : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              s.snd.base) :
          (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
        Set.univ))
    (Set.range (ι := (↑(↑(D.U j) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι j)) :
        (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))

Tactic:
exact Set.image_subset_range _ _

Premises used: Set.image_subset_range
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst

Tactic:
apply IsOpenImmersion.lift_fac

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_3 :
  Eq (α := s.pt ⟶ D.glued) (lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) ≫ D.ι i) (s.snd ≫ D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd

Tactic:
rw [← cancel_mono (𝖣.ι j), Category.assoc, ← (𝖣.vPullbackCone i j).condition]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
rw : s.fst ≫ D.ι i
| s.snd ≫ D.ι j

Tactic:
rw [← s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_3 :
  Eq (α := s.pt ⟶ D.glued) (lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) ≫ D.ι i) (s.fst ≫ D.ι i)
⊢ Eq (α := s.pt ⟶ D.glued) (lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) ≫ D.ι i) (s.snd ≫ D.ι j)

Tactic:
conv_rhs => rw [← s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_3 refine_3₁ : Eq (α := s.pt ⟶ D.glued) (s.fst ≫ D.ι i) (s.fst ≫ D.ι i)
⊢ Eq (α := s.pt ⟶ D.glued) (lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) ≫ D.ι i) (s.fst ≫ D.ι i)

Tactic:
erw [IsOpenImmersion.lift_fac_assoc]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac_assoc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
e₁ : m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
refine_4 : m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = lift (D.f i j) s.fst ⋯
⊢ m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = lift (D.f i j) s.fst ⋯

Tactic:
_
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
e₁ : m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
h : m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd
refine_4 : m ≫ D.f i j = lift (D.f i j) s.fst ⋯ ≫ D.f i j
⊢ m = lift (D.f i j) s.fst ⋯

Tactic:
rw [← cancel_mono (D.f i j)]

Premises used: CategoryTheory.GlueData.f, CategoryTheory.cancel_mono, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
e₁ : m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
h : m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd
refine_4 : m ≫ D.f i j = s.fst
⊢ m ≫ D.f i j = lift (D.f i j) s.fst ⋯ ≫ D.f i j

Tactic:
simp only [lift_fac]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
e₁ : m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
h : m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd
⊢ m ≫ D.f i j = s.fst

Tactic:
tauto
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
x : (↑(↑D.glued : TopCat) : Type v)
⊢ ∃ (i : D.J) (y : (↑(↑(D.U i) : TopCat) : Type v)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑D.glued : TopCat)) (Hom.base (D.ι i)) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y =
      x

Tactic:
𝖣.ι_jointly_surjective (PresheafedSpace.forget _ ⋙ CategoryTheory.forget TopCat) x

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.forget, TopCat, CategoryTheory.GlueData.ι_jointly_surjective, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
⊢ Eq (α := D.toPresheafedSpaceGlueData.U i ⟶ D.glued.toPresheafedSpace)
    (CategoryStruct.comp (Y := D.toPresheafedSpaceGlueData.glued)
        (D.toPresheafedSpaceGlueData.ι i : D.toPresheafedSpaceGlueData.U i ⟶ D.toPresheafedSpaceGlueData.glued)
        (Iso.inv D.isoPresheafedSpace : D.toPresheafedSpaceGlueData.glued ⟶ D.glued.toPresheafedSpace) :
      D.toPresheafedSpaceGlueData.U i ⟶ D.glued.toPresheafedSpace)
    (InducedCategory.Hom.hom (D.ι i) : (D.U i).toPresheafedSpace ⟶ D.glued.toPresheafedSpace)

Tactic:
𝖣.ι_gluedIso_inv _ _

Premises used: CategoryTheory.GlueData.ι_gluedIso_inv, CategoryTheory.GlueData.mapGlueData, AlgebraicGeometry.SheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
rw :
  PresheafedSpace.IsOpenImmersion (Y := D.glued.toPresheafedSpace)
    (CategoryStruct.comp (Y := D.toPresheafedSpaceGlueData.glued)
        (D.toPresheafedSpaceGlueData.ι i : D.toPresheafedSpaceGlueData.U i ⟶ D.toPresheafedSpaceGlueData.glued)
        (Iso.inv D.isoPresheafedSpace : D.toPresheafedSpaceGlueData.glued ⟶ D.glued.toPresheafedSpace) :
      D.toPresheafedSpaceGlueData.U i ⟶ D.glued.toPresheafedSpace)
⊢ PresheafedSpace.IsOpenImmersion (Y := D.glued.toPresheafedSpace) (InducedCategory.Hom.hom (D.ι i))

Tactic:
rw [← D.ι_isoPresheafedSpace_inv]

Premises used: AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (Y := D.toPresheafedSpaceGlueData.glued) (D.toPresheafedSpaceGlueData.ι i)

Tactic:
have := D.toPresheafedSpaceGlueData.ιIsOpenImmersion i
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
this : PresheafedSpace.IsOpenImmersion (Y := D.toPresheafedSpaceGlueData.glued) (D.toPresheafedSpaceGlueData.ι i)
⊢ PresheafedSpace.IsOpenImmersion (Y := D.glued.toPresheafedSpace)
    (CategoryStruct.comp (Y := D.toPresheafedSpaceGlueData.glued)
        (D.toPresheafedSpaceGlueData.ι i : D.toPresheafedSpaceGlueData.U i ⟶ D.toPresheafedSpaceGlueData.glued)
        (Iso.inv D.isoPresheafedSpace : D.toPresheafedSpaceGlueData.glued ⟶ D.glued.toPresheafedSpace) :
      D.toPresheafedSpaceGlueData.U i ⟶ D.glued.toPresheafedSpace)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
x : (↑(↑D.glued.toPresheafedSpace : TopCat) : Type v)
⊢ ∃ (i : D.J) (y : (↑(↑(D.U i).toPresheafedSpace : TopCat) : Type v)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑D.glued.toPresheafedSpace : TopCat)) (Hom.base (InducedCategory.Hom.hom (D.ι i))) :
          (a : (↑(↑(D.U i).toPresheafedSpace : TopCat) : Type v)) → (↑(↑D.glued.toPresheafedSpace : TopCat) : Type v))
        y =
      x

Tactic:
𝖣.ι_jointly_surjective (SheafedSpace.forget _ ⋙ CategoryTheory.forget TopCat) x

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.SheafedSpace.forget, CategoryTheory.forget, TopCat, CategoryTheory.GlueData.ι_jointly_surjective, AlgebraicGeometry.SheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
D : GlueData
i : D.J
⊢ D.toSheafedSpaceGlueData.ι i ≫ D.isoSheafedSpace.inv = Hom.toShHom (D.ι i)

Tactic:
𝖣.ι_gluedIso_inv forgetToSheafedSpace i

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData, CategoryTheory.GlueData.ι_gluedIso_inv, CategoryTheory.InducedCategory.homMk, CategoryTheory.GlueData.mapGlueData, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData
i : D.J
rw : SheafedSpace.IsOpenImmersion (D.toSheafedSpaceGlueData.ι i ≫ D.isoSheafedSpace.inv)
⊢ SheafedSpace.IsOpenImmersion (Y := D.glued.toSheafedSpace) (Hom.toShHom (D.ι i))

Tactic:
rw [← D.ι_isoSheafedSpace_inv]

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData
i : D.J
H :
  PresheafedSpace.IsOpenImmersion (Y := D.toSheafedSpaceGlueData.glued.toPresheafedSpace)
    (InducedCategory.Hom.hom (D.toSheafedSpaceGlueData.ι i))
⊢ SheafedSpace.IsOpenImmersion (D.toSheafedSpaceGlueData.ι i ≫ D.isoSheafedSpace.inv)

Tactic:
apply +allowSynthFailures PresheafedSpace.IsOpenImmersion.comp

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (Y := D.toSheafedSpaceGlueData.glued.toPresheafedSpace)
    (InducedCategory.Hom.hom (D.toSheafedSpaceGlueData.ι i))

Tactic:
(D.toSheafedSpaceGlueData).ιIsOpenImmersion i

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData, AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (Y := D.toSheafedSpaceGlueData.glued.toPresheafedSpace)
    (InducedCategory.Hom.hom (D.toSheafedSpaceGlueData.ι i))

Tactic:
exact (D.toSheafedSpaceGlueData).ιIsOpenImmersion i

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData, AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData
i j k : D.J
⊢ PreservesLimit (cospan (D.f i j) (D.f i k)) forgetToSheafedSpace

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
D : GlueData
x : (↑D.glued.toTopCat : Type u)
⊢ ∃ (i : D.J) (y : (↑(D.U i).toTopCat : Type u)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            (↑D.glued.toPresheafedSpace : TopCat)) (Hom.base (Hom.toHom (D.ι i))) :
          (a : (↑(↑(D.U i).toPresheafedSpace : TopCat) : Type u)) → (↑(↑D.glued.toPresheafedSpace : TopCat) : Type u))
        y =
      x

Tactic:
𝖣.ι_jointly_surjective
    ((LocallyRingedSpace.forgetToSheafedSpace.{u} ⋙ SheafedSpace.forget CommRingCat.{u}) ⋙
      forget TopCat.{u}) x

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData, CommRingCat, CategoryTheory.Functor.comp, AlgebraicGeometry.SheafedSpace.forget, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.forget, TopCat, CategoryTheory.GlueData.ι_jointly_surjective
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ PresheafedSpace.{v, u, v} C
j : J
U : (Opens (↑(↑(F.obj j) : TopCat) : Type v))ᵒᵖ
⊢ 𝟙 (↑(F.obj j) : TopCat) = (F.map (𝟙 j)).base

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ PresheafedSpace.{v, u, v} C
j : J
U : (Opens (↑(↑(F.obj j) : TopCat) : Type v))ᵒᵖ
⊢ (F.map (𝟙 j)).c.app U = (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom.app U

Tactic:
simp [PresheafedSpace.congr_app (F.map_id j)]

Premises used: CategoryTheory.Functor.map_id, AlgebraicGeometry.PresheafedSpace.congr_app
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens (↑(↑(F.obj j₃) : TopCat) : Type v))ᵒᵖ
⊢ (F.map (f ≫ g)).c.app U =
    (F.map g).c.app U ≫
      NatTrans.app (map (pushforward C (F.map g).base) (F.map f).c) U ≫
        NatTrans.app (Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf)) U

Tactic:
simp [PresheafedSpace.congr_app (F.map_comp f g)]

Premises used: CategoryTheory.Functor.map_comp, AlgebraicGeometry.PresheafedSpace.congr_app
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ PresheafedSpace.{v, u, v} C
inst_2 : HasColimit F
U : Opens (↑(↑(colimit F) : TopCat) : Type v)
j k : Jᵒᵖ
f : j ⟶ k
rw :
  (Opens.map (F.map f.unop).base).op.obj (op (obj (Opens.map (Hom.base (colimit.ι F (unop j)))) U)) =
    op (obj (Opens.map ((F.map f.unop).base ≫ Hom.base (colimit.ι F (unop j)))) U)
⊢ (Opens.map (F.map f.unop).base).op.obj (op (obj (Opens.map (Hom.base (colimit.ι F (unop j)))) U)) =
    op (obj (Opens.map (Hom.base (colimit.ι F (unop k)))) U)

Tactic:
rw [← colimit.w F f.unop, comp_base]

Premises used: Quiver.Hom.unop, AlgebraicGeometry.PresheafedSpace.comp_base, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ PresheafedSpace.{v, u, v} C
inst_2 : HasColimit F
U : Opens (↑(↑(colimit F) : TopCat) : Type v)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op (obj (Opens.map (Hom.base (colimit.ι F (unop j)))) U)) =
    op (obj (Opens.map ((F.map f.unop).base ≫ Hom.base (colimit.ι F (unop j)))) U)

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ PresheafedSpace.{v, u, v} C
inst_2 : HasColimit F
U : Opens (↑(↑(colimit F) : TopCat) : Type v)
i j k : Jᵒᵖ
f : i ⟶ j
g : j ⟶ k
simp :
  (F.map (f ≫ g).unop).c.app (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U)) ≫
      (F.obj (unop k)).presheaf.map (eqToHom ⋯) =
    (F.map f.unop).c.app (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U)) ≫
      (F.map g.unop).c.app
          ((Opens.map (F.map f.unop).base).op.obj (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U))) ≫
        (obj (pushforward C (F.map g.unop).base) (F.obj (unop k)).presheaf).map (eqToHom ⋯) ≫
          (F.obj (unop k)).presheaf.map (eqToHom ⋯)
⊢ (F.map (f ≫ g).unop).c.app (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U)) ≫
      (F.obj (unop k)).presheaf.map (eqToHom ⋯) =
    ((F.map f.unop).c.app (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U)) ≫
        (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map g.unop).c.app (op (obj (Opens.map (Hom.base (colimit.ι F (unop j)))) U)) ≫
        (F.obj (unop k)).presheaf.map (eqToHom ⋯)

Tactic:
simp only [assoc, CategoryTheory.NatTrans.naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ PresheafedSpace.{v, u, v} C
inst_2 : HasColimit F
U : Opens (↑(↑(colimit F) : TopCat) : Type v)
i j k : Jᵒᵖ
f : i ⟶ j
g : j ⟶ k
⊢ (F.map (f ≫ g).unop).c.app (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U)) ≫
      (F.obj (unop k)).presheaf.map (eqToHom ⋯) =
    (F.map f.unop).c.app (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U)) ≫
      (F.map g.unop).c.app
          ((Opens.map (F.map f.unop).base).op.obj (op (obj (Opens.map (Hom.base (colimit.ι F (unop i)))) U))) ≫
        (obj (pushforward C (F.map g.unop).base) (F.obj (unop k)).presheaf).map (eqToHom ⋯) ≫
          (F.obj (unop k)).presheaf.map (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
F : J ⥤ PresheafedSpace.{v, u, v} C
j : J
a :
  Eq (α :=
    Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
        (Quiver.Hom.op
          (map (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.map (𝟙 j)).c ≫
            Iso.inv (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf) ≫
              Iso.hom (pushforwardEq ⋯ (F.obj j).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
        (𝟙 (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))))
⊢ Eq (α :=
    Quiver.Hom (V := (Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))ᵒᵖ)
      (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf))
      (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))
    (Quiver.Hom.op
      (map (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.map (𝟙 j)).c ≫
        Iso.inv (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf) ≫
          Iso.hom (pushforwardEq ⋯ (F.obj j).presheaf)))
    (𝟙 (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j)) (F.obj j).presheaf)))

Tactic:
apply (opEquiv _ _).injective

Premises used: CategoryTheory.opEquiv, Equiv.injective