mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j ≫ (ρ_ (F.obj j)).hom = 𝟙 (F.obj j)

Tactic:
← rightUnitor_hom_app,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j ≫ (ρ_ F).hom.app j = 𝟙 (F.obj j)
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝³ : SmallCategory C
D : Type u
inst✝² : SmallCategory D
inst✝¹ : IsSifted C
F : C ⥤ D
inst✝ : F.Final
⊢ IsSifted D

Tactic:
by
  have : PreservesFiniteProducts (colim : (D ⥤ Type u) ⥤ _) :=
    ⟨fun n ↦ preservesLimitsOfShape_of_natIso (Final.colimIso F)⟩
  exact of_colim_preservesFiniteProducts D

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'

Tactic:
intro _ c _ _
      exact ⟨ c, 𝟙 _, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit G ≅ colimit (uncurry.obj (curry.obj G))

pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit (uncurry.obj (curry.obj G)) ≅ colimit (curry.obj G ⋙ colim)

Tactic:
· apply HasColimit.isoOfNatIso i

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit (uncurry.obj (curry.obj G)) ≅ colimit (curry.obj G ⋙ colim)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
U : Cᵒᵖ
a₁ a₂ : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 a₁_1 a₂_1 x_1,
    (ιR cR) a₁_1 =
        ((ConcreteCategory.hom
              ((((forget RingCat).mapCocone cR).tensor
                      (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                U))
            (a₁, a₂, x)).1 ∧
      (ιR cR) a₂_1 =
          ((ConcreteCategory.hom
                  ((((forget RingCat).mapCocone cR).tensor
                          (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                    U))
                (a₁, a₂, x)).2.1 ∧
        ιM x_1 =
          ((ConcreteCategory.hom
                  ((((forget RingCat).mapCocone cR).tensor
                          (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                    U))
                (a₁, a₂, x)).2.2

Tactic:
exact ⟨U, a₁, a₂, x, rfl, rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
N : ModuleCat ↑cR.pt
α : ModuleColimit hcR hcM →+ ↑N
h :
  ∀ (U : Cᵒᵖ) (r : ↑(R.obj U)) (m : ↑(M.obj U)),
    (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) (r • m) =
      (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) m
r : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ α (r • m) = r • α m

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
N : ModuleCat ↑cR.pt
α : ModuleColimit hcR hcM →+ ↑N
h : ∀ (r : ↑cR.pt) (m : ModuleColimit hcR hcM), α (r • m) = r • α m
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) m

Tactic:
· obtain ⟨U, r, m, rfl, rfl⟩ := jointly_surjective₂ r m
    refine Eq.trans ?_ ((homEquiv'_app_apply ..).symm.trans (h U r m))
    congr 1
    apply smul_eq

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
N : ModuleCat ↑cR.pt
α : ModuleColimit hcR hcM →+ ↑N
h : ∀ (r : ↑cR.pt) (m : ModuleColimit hcR hcM), α (r • m) = r • α m
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
r : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) (r • m) =
    (RingHom.id ↑cR.pt) r • (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) m

Tactic:
obtain ⟨U, r, m, rfl, rfl⟩ := ModuleColimit.jointly_surjective₂ r m

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) ((ιR cR) r • ιM m) =
    (RingHom.id ↑cR.pt) ((ιR cR) r) •
      (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) (ιM m)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ◁ x✝ ≫ (λ_ Y✝).hom).app X✝ = ((λ_ X✝¹).hom ≫ x✝).app X✝

Tactic:
apply leftUnitor_naturality

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝ ⟶ Y✝
⊢ x✝ ▷ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ≫ (ρ_ Y✝).hom = (ρ_ X✝).hom ≫ x✝

Tactic:
by ext1; apply rightUnitor_naturality

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
⊢ Sieve.pullback h S ∈ {S | ∃ Y_1 f, S.arrows f}

Tactic:
rcases hro h f with ⟨W, g, k, comm⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ Sieve.pullback h S ∈ {S | ∃ Y_1 f, S.arrows f}
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ Presieve.singleton (f ≫ g) K → (Presieve.singleton g).bind Ti K

Tactic:
rintro ⟨_⟩
      refine bind_comp g singleton.mk ?_
      rw [hTi]
      apply singleton.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
⊢ x.sieveExtend f ⋯ = x f hf

Tactic:
have h := (le_generate R Y _ hf).choose_spec

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ x.sieveExtend f ⋯ = x f hf
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Z : D
u : Z ⟶ F.obj X
⊢ (generate (Presieve.map F s)).arrows u → Presieve.functorPushforward F s u

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Z : D
u : Z ⟶ F.obj X
⊢ Presieve.functorPushforward F s u → (generate (Presieve.map F s)).arrows u

Tactic:
· rintro ⟨_, _, _, ⟨hu⟩, rfl⟩; exact ⟨_, _, _, hu, rfl⟩

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Z : D
u : Z ⟶ F.obj X
⊢ Presieve.functorPushforward F s u → (generate (Presieve.map F s)).arrows u
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
⊢ (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x

Tactic:
apply SecondObj.ext

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
⊢ ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (secondMap P S)) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
⊢ (∃! a_1, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a_1 = S.shrinkFunctorIsoFunctor.homFromEquiv.symm a) ↔
    ∃! g, S.functorInclusion ≫ g = a

Tactic:
rw [Equiv.existsUnique_congr_left (shrinkYonedaIsoYoneda.app X).homFromEquiv]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
⊢ (∃! b,
      (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (shrinkYonedaIsoYoneda.app X).homFromEquiv.symm b =
        S.shrinkFunctorIsoFunctor.homFromEquiv.symm a) ↔
    ∃! g, S.functorInclusion ≫ g = a
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows

Tactic:
constructor
  · intro hs E x t₁ t₂ h₁ h₂
    have hx := is_compatible_of_exists_amalgamation x ⟨t₁, h₁⟩
    rw [compatible_iff_sieveCompatible] at hx
    specialize hs hx.cone
    rcases hs with ⟨hs⟩
    simpa only [Subtype.mk.injEq] using (show Subtype.mk t₁ h₁ = ⟨t₂, h₂⟩ from
      (homEquivAmalgamation hx).symm.injective (hs _ _))
  · rintro h ⟨E, π⟩
    let eqv := conesEquivSieveCompatibleFamily P S (op E)
    constructor
    rw [← eqv.left_inv π]
    intro f₁ f₂
    let eqv' := homEquivAmalgamation (eqv π).2
    apply eqv'.injective
    ext
    apply h _ (eqv π).1 <;> exact (eqv' _).2

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ (fun t ↦ x.IsAmalgamation t) (x (𝟙 X) ⋯)

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∀ (y : P.obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = x (𝟙 X) ⋯

Tactic:
· rintro _ _ ⟨rfl, rfl⟩
    simp

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∀ (y : P.obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = x (𝟙 X) ⋯
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom ((P ⋙ coyoneda.obj (op X)).map f.op))
      (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯) =
    z f hf

Tactic:
apply ConcreteCategory.hom_ext

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
hf : S.arrows f
⊢ ∀ (x : unop (op X)),
    (ConcreteCategory.hom
          ((ConcreteCategory.hom ((P ⋙ coyoneda.obj (op X)).map f.op))
            (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)))
        x =
      (ConcreteCategory.hom (z f hf)) x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
⊢ y = ↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯

Tactic:
apply ConcreteCategory.hom_ext

Goal state after:
case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
⊢ ∀ (x : unop (op X)),
    (ConcreteCategory.hom y) x =
      (ConcreteCategory.hom (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)) x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
⊢ IsTerminal (F.obj.obj (op X))

Tactic:
by
  refine @IsTerminal.ofUnique _ _ _ ?_
  intro Y
  choose t h using F.2 Y _ H (by tauto) (by tauto)
  exact ⟨⟨t⟩, fun a => h.2 a (by tauto)⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
simp only [← isOpen_coinduced]
    apply isOpen_iSup_iff

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ Small.{u, max u v} (F ⋙ forget).ColimitType

Tactic:
rw [← Types.hasColimit_iff_small_colimitType]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ HasColimit (F ⋙ forget)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
ι : Type u_5
inst✝ : Category.{v_2, u_3} C
F G : Discrete ι ⥤ C
α : F ⟶ G
⊢ Equifibered α

Tactic:
by
  rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
  simp only [Discrete.functor_map_id]
  exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
inst✝ : Category.{v_2, u_3} C
ι : Type u_6
F G : Discrete ι ⥤ C
α : F ⟶ G
⊢ Equifibered α

Tactic:
by
  rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
  simp only [Discrete.functor_map_id]
  exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_3.snd
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).2 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).2

Tactic:
simpa using! ConcreteCategory.congr_hom h₂ x

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case e'_5
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
e_1✝ : ↑(range ⇑(ConcreteCategory.hom c.inl))ᶜ = { a // a ∉ range ⇑(ConcreteCategory.hom c.inl) }
⊢ ((range ⇑(ConcreteCategory.hom c.inl))ᶜ.domRestrict fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑⋯.toHomeomorph.symm ∘ Subtype.map (fun a ↦ a) this

Tactic:
ext ⟨x, hx⟩
              exact dif_neg hx

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan (X ∘ Sum.inl)
c₂ : Cofan (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst✝ : MonoCoprod C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono inr

Tactic:
rw [this]
    exact MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasCoproducts C
inst✝ : MonoCoprod C
J I : Type u
ι : J ⟶ I
hι : Mono ι
⊢ Mono ((sigmaConst.obj A).map ι)

Tactic:
by
    rw [mono_iff_injective] at hι
    exact MonoCoprod.mono_map'_of_injective (fun (i : I) ↦ A) ι hι

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: case x
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ (j : J) → ((curry.obj (swap K J ⋙ F)).obj k'').obj j

Tactic:
exact fun j => F.map (𝟙 j ×ₘ (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) (y j)

Goal state after: