mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op ≫ P.map (pullback.lift gi gj comm).op)) (x j) =
    (ConcreteCategory.hom (P.map gj.op)) (x j)

Tactic:
← Functor.map_comp,

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map ((pullback.snd (π i) (π j)).op ≫ (pullback.lift gi gj comm).op))) (x j) =
    (ConcreteCategory.hom (P.map gj.op)) (x j)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (ConcreteCategory.hom (F.map (i₁ V₁ g₃ S₁).op ≫ F.map g₁.op)) ↑(x (i₂ V₁ g₃ S₁) ⋯) =
    (ConcreteCategory.hom (F.map g₂.op)) (x'' g₄ S₂)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (ConcreteCategory.hom (F.map ((i₁ V₁ g₃ S₁).op ≫ g₁.op))) ↑(x (i₂ V₁ g₃ S₁) ⋯) =
    (ConcreteCategory.hom (F.map g₂.op)) (x'' g₄ S₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y✝ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y✝ hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y✝ hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y✝ hf).IsAmalgamation (t f hf)
hT : t.Compatible
y : P.obj (op X)
hy : s.IsAmalgamation y
Y : C
f : Y ⟶ X
hf : U.arrows f
Z : C
g : Z ⟶ Y
hg : (B hf).arrows g
⊢ (ConcreteCategory.hom (P.map f.op ≫ P.map g.op)) y =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (P.map f.op)) (hU.amalgamate t hT))

Tactic:
← Functor.map_comp,

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y✝ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y✝ hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y✝ hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y✝ hf).IsAmalgamation (t f hf)
hT : t.Compatible
y : P.obj (op X)
hy : s.IsAmalgamation y
Y : C
f : Y ⟶ X
hf : U.arrows f
Z : C
g : Z ⟶ Y
hg : (B hf).arrows g
⊢ (ConcreteCategory.hom (P.map (f.op ≫ g.op))) y =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (P.map f.op)) (hU.amalgamate t hT))
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom)) ≫ I.m.hom =
    (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι

Tactic:
generalize_proofs h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
pf✝ : IsIso (Subfunctor.toRange I.m.hom)
⊢ (Subfunctor.homOfLe h ≫ inv (Subfunctor.toRange I.m.hom)) ≫ I.m.hom =
    (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
⊢ Nonempty (IsLimit c) ↔ c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str

Tactic:
refine ⟨fun ⟨hc⟩ ↦ induced_of_isLimit _ hc, fun h ↦ ⟨?_⟩⟩

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ IsLimit c
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
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
let c' := coconeOfCoconeForget ((forget).mapCocone c)

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝¹ : PreservesLimitsOfShape WalkingCospan G
inst✝ : ReflectsColimitsOfShape J G
hc : IsUniversalColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
j : J
⊢ (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ (const J).map (G.map f)).app j

Tactic:
simpa using! G.congr_map (NatTrans.congr_app h j)

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₂
T✝ : C
f₁ : c₁.pt ⟶ T✝
f₂ : c₂.pt ⟶ T✝
m : (binaryCofanSum c c₁ c₂ hc₁ hc₂).pt ⟶ T✝
hm₁ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl ≫ m = f₁
hm₂ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr ≫ m = f₂
⊢ ∀ (i : I₁ ⊕ I₂),
    c.inj i ≫ m =
      c.inj i ≫
        Cofan.IsColimit.desc hc fun i ↦
          match i with
          | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
          | Sum.inr i₂ => c₂.inj i₂ ≫ f₂

Tactic:
rintro (i₁ | i₂) <;> cat_disch

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

Goal state before:
pp: J : Type v'
inst✝⁷ : Category.{u', v'} J
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝⁴ : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst✝³ : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst✝² : ReflectsLimitsOfShape WalkingCospan G
inst✝¹ : PreservesColimitsOfShape J G
inst✝ : ReflectsColimitsOfShape J G
H : IsVanKampenColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
j : J
⊢ (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ (const J).map (G.map f)).app j

Tactic:
simpa using! G.congr_map (NatTrans.congr_app h j)

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

Goal state before:
pp: J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
⊢ α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f →
    NatTrans.Equifibered α →
      (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)) → Nonempty (IsColimit c')

Tactic:
e'

Goal state after:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
⊢ NatTrans.Equifibered α →
    (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)) → Nonempty (IsColimit c')
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k ↦ X ↑k
⊢ Mono (Sigma.map' ι fun j ↦ 𝟙 ((X ∘ ι) j))

Tactic:
convert! mono_of_injective' X ι hι

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k ↦ X ↑k
⊢ (Sigma.map' ι fun j ↦ 𝟙 ((X ∘ ι) j)) = Sigma.desc fun j ↦ Sigma.ι X (ι j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
⊢ α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f →
    NatTrans.Equifibered α →
      (Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j))

Tactic:
e'

Goal state after:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
⊢ NatTrans.Equifibered α →
    (Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j))
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
rintro ⟨hc'⟩ j

Goal state after:
case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: 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' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f ≫ i f))) (y j) =
    (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f) ≫ F.map (𝟙 j' ×ₘ i f))) (y j)

Tactic:
← Functor.map_comp,

Goal state after:
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' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f ≫ i f))) (y j) =
    (ConcreteCategory.hom (F.map ((f ×ₘ g j ≫ hf f) ≫ (𝟙 j' ×ₘ i f)))) (y j)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: 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' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f) ≫ F.map (𝟙 j' ×ₘ i f))) (y j') =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f ≫ i f))) (y j')

Tactic:
← Functor.map_comp,

Goal state after:
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' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map ((𝟙 j' ×ₘ g j' ≫ gf f) ≫ (𝟙 j' ×ₘ i f)))) (y j') =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f ≫ i f))) (y j')
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
by
  let f : Fin n → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  induction n with
  | zero => exact isVanKampenColimit_of_isEmpty _ hc
  | succ n IH =>
    apply IsVanKampenColimit.of_iso _
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
    apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_
    · apply IH
      exact coproductIsCoproduct _
    · apply FinitaryExtensive.van_kampen'
      exact coprodIsCoprod _ _
    · dsimp
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) := ⋯
⊢ Nonempty (IsColimit c)

Tactic:
refine IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
      (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i)
      ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
      (fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)

Goal state after:
case refine_1
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) :=
  Cofan.mk (pullback (Sigma.desc f) (Sigma.desc g)) fun p ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsUniversalColimit (Cofan.mk (∐ X) fun i ↦ Sigma.ι X i)

case refine_2
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) :=
  Cofan.mk (pullback (Sigma.desc f) (Sigma.desc g)) fun p ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsUniversalColimit (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i)

case refine_3
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) :=
  Cofan.mk (pullback (Sigma.desc f) (Sigma.desc g)) fun p ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsLimit (pullback.cone (Sigma.desc f) (Sigma.desc g))