mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case left
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
⊢ Mono (Cofan.inj c WalkingPair.left)

pp: case right
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
⊢ Mono (Cofan.inj c WalkingPair.right)

Tactic:
· exact inferInstanceAs <| Mono c.inl

Goal state after:
case right
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
⊢ Mono (Cofan.inj c WalkingPair.right)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ i ∧ IsPullback i' αY αZ h

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback αX h' i αZ ∧ IsPullback αY i' h αZ
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
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
k : K
⊢ ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app k =
    ((Cocone.whisker e.inverse c').ι ≫ (const K).map f).app k

Tactic:
simpa using

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
hα : NatTrans.Equifibered α
k : K
⊢ α.app (e.inverse.obj k) ≫ c.ι.app (e.functor.obj (e.inverse.obj k)) = c'.ι.app (e.inverse.obj k) ≫ f
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_1.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ c.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr

Tactic:
rw [← H.w_assoc]; erw [h.fac _ ⟨WalkingPair.right⟩]; exact s.condition

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✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
X : ι → C
⊢ CoproductDisjoint X

Tactic:
refine ⟨fun {c} hc i j e s hs ↦ ?_, fun hc i ↦ FinitaryExtensive.mono_ι hc ⟨i⟩⟩
    exact ⟨initialIsInitial.ofIso ((FinitaryExtensive.isPullback_initial_to hc ⟨i⟩ ⟨j⟩
      (by simpa)).isoIsPullback _ _ (IsPullback.of_isLimit hs))⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (𝟙 A) (𝟙 A)).ι.app j) ((mapPair f f).app j) f
      ((BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι.app j)

Tactic:
rintro ⟨⟨⟩⟩ <;> dsimp

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsPullback (𝟙 A) f f (𝟙 (⊥_ C))

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsPullback (𝟙 A) f f (𝟙 (⊥_ C))
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G').app (L₁.obj X₁) ≫
      (G'.associator F' G').hom.app (L₁.obj X₁) ≫ (G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app (L₁.obj X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
whiskerRight_app,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map ((Localization.ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁)) ≫
      (G'.associator F' G').hom.app (L₁.obj X₁) ≫ (G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app (L₁.obj X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      (F'.associator G' F').inv.app (L₂.obj X₂) ≫
        (whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F').app (L₂.obj X₂) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
whiskerRight_app,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      (F'.associator G' F').inv.app (L₂.obj X₂) ≫ F'.map ((Localization.η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isColocal f
hg : P.isColocal g
X : C
hX : P X
⊢ Function.Bijective fun f_1 ↦ f_1 ≫ f ≫ g

Tactic:
by
    convert! Function.Bijective.comp (hg X hX) (hf X hX)
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ ⋯.IsVanKampen

Tactic:
apply Adhesive.van_kampen

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ ⋯.IsVanKampen

Tactic:
apply Adhesive.van_kampen

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
⊢ J.W = (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage G

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj]

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

Goal state before:
pp: case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x y : ToType (F.obj X)
h : equalizerSieve x y = ⊤
⊢ x = y

Tactic:
simpa using

Goal state after:
case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x y : ToType (F.obj X)
h : equalizerSieve x y = ⊤
⊢ x = y
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
⊢ IsLocallyInjective J φ → IsLocallyInjective J (Functor.whiskerRight φ (forget D))

Tactic:
· intro
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : HasWeakSheafify J A
inst✝ : J.PreservesSheafification F
X : Cᵒᵖ ⥤ A
⊢ IsIso ((presheafToSheaf J B).map (whiskerRight (toSheafify J X) F))

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : HasWeakSheafify J A
inst✝ : J.PreservesSheafification F
X : Cᵒᵖ ⥤ A
⊢ J.W (whiskerRight (toSheafify J X) F)
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J φ
inst✝ : IsLocallyInjective J ψ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom ((φ ≫ ψ).app X)) x = (ConcreteCategory.hom ((φ ≫ ψ).app X)) y
⊢ (ConcreteCategory.hom (ψ.app X)) ((ConcreteCategory.hom (φ.app X)) x) =
    (ConcreteCategory.hom (ψ.app X)) ((ConcreteCategory.hom (φ.app X)) y)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J φ
inst✝ : IsLocallyInjective J ψ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom ((φ ≫ ψ).app X)) x = (ConcreteCategory.hom ((φ ≫ ψ).app X)) y
⊢ (ConcreteCategory.hom (ψ.app X)) ((ConcreteCategory.hom (φ.app X)) x) =
    (ConcreteCategory.hom (ψ.app X)) ((ConcreteCategory.hom (φ.app X)) y)
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsLocallyInjective J (φ ≫ ψ)
⊢ IsLocallyInjective J φ

Tactic:
exact isLocallyInjective_of_isLocallyInjective J φ ψ

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₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (f₁ ≫ f₂) x).arrows g
⊢ (ConcreteCategory.hom (f₂.app (op Y))) ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) x g hg)) =
    (ConcreteCategory.hom (F₃.map g.op)) x

Tactic:
simpa using

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₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (f₁ ≫ f₂) x).arrows g
⊢ (ConcreteCategory.hom (f₂.app (op Y))) ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) x g hg)) =
    (ConcreteCategory.hom (F₃.map g.op)) x
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_1
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₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦ equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop X
hg : S.arrows g
ha : (T g hg).arrows a
⊢ (equalizerSieve x₁ x₂).arrows (a ≫ g)

Tactic:
simpa using

Goal state after:
case refine_1
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₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦ equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop X
hg : S.arrows g
ha : (T g hg).arrows a
⊢ (ConcreteCategory.hom (F₂.map a.op)) ((ConcreteCategory.hom (F₂.map g.op)) x₁) =
    (ConcreteCategory.hom (F₂.map a.op)) ((ConcreteCategory.hom (F₂.map g.op)) x₂)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
X Y : Cᵒᵖ
hX : Limits.IsInitial X
hY : Limits.IsInitial Y
φ : X ≅ Y
M : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (R.obj.map (hX.to U)) =
    (RingCat.Hom.hom (R.obj.map (hY.to U))).comp (RingCat.Hom.hom (R.obj.map φ.hom))

Tactic:
simpa using

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
X Y : Cᵒᵖ
hX : Limits.IsInitial X
hY : Limits.IsInitial Y
φ : X ≅ Y
M : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (R.obj.map (hX.to U)) =
    (RingCat.Hom.hom (R.obj.map (hY.to U))).comp (RingCat.Hom.hom (R.obj.map φ.hom))
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case mpr
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₂ → IsLocallyInjective J (f₁ ≫ f₂)

Tactic:
· intro
    infer_instance

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

Goal state before:
pp: case mpr
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₂
⊢ IsLocallySurjective J f₁ → IsLocallySurjective J (f₁ ≫ f₂)

Tactic:
· 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₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : s ∈ (Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)
⊢ (Subfunctor.range f).sieveOfSection s ≤ imageSieve (Subfunctor.toRangeSheafify J f) ⟨s, hs⟩

Tactic:
rintro Y g ⟨t, ht⟩

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₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : s ∈ (Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)
Y : C
g : Y ⟶ X
t : F₁.obj (op Y)
ht : (ConcreteCategory.hom (f.app (op Y))) t = (ConcreteCategory.hom (F₂.map g.op)) s
⊢ (imageSieve (Subfunctor.toRangeSheafify J f) ⟨s, hs⟩).arrows g
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ IsLocallySurjective φ → Epi φ

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ Epi φ → IsLocallySurjective φ

Tactic:
· intro
    infer_instance

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ Epi φ → IsLocallySurjective φ
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a : V ⟶ X i
hw :
  (ConcreteCategory.hom ((Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)).app (op V)))
      ((ConcreteCategory.hom ((((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).ι.app { as := i }))
        (shrinkYonedaObjObjEquiv.symm a)) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
⊢ shrinkYonedaObjObjEquiv.symm (v ≫ g) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)

Tactic:
· exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (PullbackCone.IsLimit.lift ht (s j.as).fst ((s j.as).snd ≫ a.inj j.as) ⋯ ≫ t.fst) (s j.as).snd v
    (a.inj j.as ≫ u)

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (s j.as).fst (s j.as).snd v (f j.as)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (PullbackCone.IsLimit.lift ht ((s j.as).fst ≫ a.inj j.as) (s j.as).snd ⋯ ≫ t.snd) (s j.as).fst v
    (a.inj j.as ≫ u)

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (s j.as).snd (s j.as).fst v (f j.as)