mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ⋯
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
⊢ (TypeCat.homEquiv.symm fun x ↦ x') ≫ (Fork.ofι f w).ι =
    TypeCat.homEquiv.symm ⇑(hom ↑(Fork.IsLimit.lift' t y' hy')) ≫ (Fork.ofι f w).ι

Tactic:
ext ⟨⟩

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
⊢ (hom ((TypeCat.homEquiv.symm fun x ↦ x') ≫ (Fork.ofι f w).ι)).toFun PUnit.unit =
    (hom (TypeCat.homEquiv.symm ⇑(hom ↑(Fork.IsLimit.lift' t y' hy')) ≫ (Fork.ofι f w).ι)).toFun PUnit.unit
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
⊢ ∀ (m : S.arrows.cocone.pt ⟶ s.pt),
    (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ m = s.ι.app j) → m = Exists.choose ⋯

Tactic:
Fs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
⊢ (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j) → Fs = Exists.choose ⋯
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
this : HasPullback f₁ f₂
⊢ pullback.fst f₁ f₂ ≫ f₁ = pullback.snd f₁ f₂ ≫ f₂

Tactic:
apply pullback.condition

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 : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
⊢ x.sieveExtend.Compatible

Tactic:
intro _ _ _ _ _ _ _ h₁ h₂ comm
  simp only [FamilyOfElements.sieveExtend, ← comp_apply, ← Functor.map_comp, ← op_comp]
  apply hx
  simp [comm, h₁.choose_spec.choose_spec.choose_spec.2, h₂.choose_spec.choose_spec.choose_spec.2]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
⊢ ofArrows Y f = ofObjects Y X

Tactic:
by
  refine le_antisymm (ofArrows_le_ofObjects Y f) (fun W g => ?_)
  rw [mem_ofArrows_iff, mem_ofObjects_iff]
  rintro ⟨i, ⟨h⟩⟩
  exact ⟨i, h, hX.hom_ext _ _⟩

Goal state after:
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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)
⊢ ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (firstMap P R)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (secondMap P R)) x)

Tactic:
rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ (ConcreteCategory.hom
        (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
          { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }))
      ((ConcreteCategory.hom (firstMap P R)) x) =
    (ConcreteCategory.hom
        (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
          { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }))
      ((ConcreteCategory.hom (secondMap P R)) 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₁
⊢ IsSheafFor P S.arrows ↔ YonedaSheafCondition P S

Tactic:
rw [isSheafFor_iff_bijective_shrinkFunctor_ι_comp, YonedaSheafCondition,
    Function.bijective_iff_existsUnique,
    Equiv.forall_congr_left S.shrinkFunctorIsoFunctor.homFromEquiv]

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

Goal state before:
pp: case mpr
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
⊢ z.Compatible → ∃! t, z.IsAmalgamation t

Tactic:
hz

Goal state after:
case mpr
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
⊢ ∃! t, z.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.sheafificationWhiskerLeftIso P).hom.app F = (J.sheafifyCompIso F P).hom

Tactic:
by
  dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso]
  simp only [sheafify, Category.comp_id]

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

Goal state before:
pp: case e_a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
a : (unop W).shape.L
⊢ (F.map
          (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
            (fun x ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) ≫
        (J.diagramCompIso F Q (unop X)).hom.app W) ≫
      Multiequalizer.ι ((unop W).index (Q ⋙ F)) a =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      Multiequalizer.ι ((unop W).index (Q ⋙ F)) a

Tactic:
simp only [diagramCompIso_hom_ι_assoc, Multiequalizer.lift_ι, diagramCompIso_hom_ι,
    Category.assoc]

Goal state after:
case e_a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
a : (unop W).shape.L
⊢ F.map
        (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
          (fun x ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) ≫
      F.map (Multiequalizer.ι ((unop W).index Q) a) =
    F.map (Multiequalizer.ι ((unop W).index P) a) ≫ F.map (η.app (op a.Y))
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
⊢ ⇑(ConcreteCategory.hom g) = ⇑(ConcreteCategory.hom (f ≫ g)) ∘ ⇑(homeoOfIso (asIso f).symm)

Tactic:
exact congr_arg (DFunLike.coe ∘ ConcreteCategory.hom) (IsIso.inv_hom_id_assoc f g).symm

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✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
le_iInf_iff

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: X : TopCat
f : of PEmpty.{u + 1} ⟶ X
⊢ f = default

Tactic:
ext ⟨⟩

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

Goal state before:
pp: case mpr
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)
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩

Goal state after:
case mpr.refine_1
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} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)

case mpr.refine_2
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), c.inl ≫ ?mpr.refine_1 f g = f

case mpr.refine_3
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), c.inr ≫ ?mpr.refine_1 f g = g

case mpr.refine_4
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) (m : c.pt ⟶ T), c.inl ≫ m = f → c.inr ≫ m = g → m = ?mpr.refine_1 f g
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case refine_1
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
s : Set ↑c.pt
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' s) ↔ IsOpen s

pp: case refine_2
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective ⇑(ConcreteCategory.hom c.π)

Tactic:
· exact (isOpen_iff_of_isColimit_cofork c hc s).symm

Goal state after:
case refine_2
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective ⇑(ConcreteCategory.hom c.π)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (A B : C), ∃ c x, Mono c.inl
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
⊢ Mono c'.inl

Tactic:
obtain ⟨c, hc₁, hc₂⟩ := h A B

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (A B : C), ∃ c x, Mono c.inl
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono c.inl
⊢ Mono c'.inl
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
X Y : C
c : Cocone (pair X Y)
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
exact FinitaryExtensive.van_kampen' c hc

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
⊢ FinitaryExtensive (Type u)

Tactic:
rw [finitaryExtensive_iff_of_isTerminal (Type u) PUnit Types.isTerminalPUnit _
      (Types.binaryCoproductColimit _ _)]

Goal state after:
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
⊢ IsVanKampenColimit (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
j : J
⊢ Gl.map (Gr.map (α.app j ≫ 𝟙 (Gl.obj (Gr.obj (F.obj j))) ≫ adj.counit.app (F.obj j) ≫ 𝟙 (F.obj j))) ≫
      adj.counit.app (F.obj j) =
    (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)

Tactic:
simp only [Category.comp_id, Adjunction.counit_naturality_assoc, Category.id_comp,
      Adjunction.counit_naturality, Category.assoc, Functor.map_comp]

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
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j✝ : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
j : J
⊢ Gl.map (Gr.map (α.app j ≫ 𝟙 (Gl.obj (Gr.obj (F.obj j))) ≫ adj.counit.app (F.obj j) ≫ 𝟙 (F.obj j))) ≫
      adj.counit.app (F.obj j) =
    (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)

Tactic:
simp only [Category.comp_id, Adjunction.counit_naturality_assoc, Category.id_comp,
      Adjunction.counit_naturality, Category.assoc, Functor.map_comp]

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

Goal state before:
pp: case mp.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inr (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) c.inr

Tactic:
have : IsIso (𝟙 Y') := inferInstance

Goal state after:
case mp.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
this : IsIso (𝟙 Y')
⊢ IsPullback c'.inr (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) c.inr
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J f₁
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallyInjective J (f₁ ≫ f₂) ↔ IsLocallyInjective J f₂

Tactic:
by
  constructor
  · intro
    exact isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂
  · intro
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁✝ F₂✝ F₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj.obj (op Y)
hs : (ConcreteCategory.hom (φ.hom.app (op Y))) s = (ConcreteCategory.hom (F₂.obj.map f.op)) x
h₁ :
  (ConcreteCategory.hom (f₁.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)) x)
h₂ :
  (ConcreteCategory.hom (f₂.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)) x)
⊢ (ConcreteCategory.hom (f₁.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (f₂.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x)

Tactic:
← hs

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁✝ F₂✝ F₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj.obj (op Y)
hs : (ConcreteCategory.hom (φ.hom.app (op Y))) s = (ConcreteCategory.hom (F₂.obj.map f.op)) x
h₁ :
  (ConcreteCategory.hom (f₁.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)) x)
h₂ :
  (ConcreteCategory.hom (f₂.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)) x)
⊢ (ConcreteCategory.hom (f₁.hom.app (op Y))) ((ConcreteCategory.hom (φ.hom.app (op Y))) s) =
    (ConcreteCategory.hom (f₂.hom.app (op Y))) ((ConcreteCategory.hom (φ.hom.app (op Y))) s)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.refine_1.isTrue
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
j : ι
h✝ : j = i
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

pp: case refine_2.refine_1.isFalse
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
j : ι
h✝ : ¬j = i
⊢ (eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

Tactic:
· subst ‹j = i›; simp

Goal state after:
case refine_2.refine_1.isFalse
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
j : ι
h✝ : ¬j = i
⊢ (eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j