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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (y : FirstObj P X),
      (ConcreteCategory.hom (firstMap P X π)) y = (ConcreteCategory.hom (secondMap P X π)) y →
        ∃! x, (ConcreteCategory.hom (forkMap P X π)) x = y

Tactic:
simp only [FirstObj]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (y : ∏ᶜ fun i ↦ P.obj (op (X i))),
      (ConcreteCategory.hom (firstMap P X π)) y = (ConcreteCategory.hom (secondMap P X π)) y →
        ∃! x, (ConcreteCategory.hom (forkMap P X π)) x = y
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: 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)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
⊢ t (h ≫ f) ⋯ = (ConcreteCategory.hom (P.map h.op)) (t f hf)

Tactic:
apply (hB (U.downward_closed hf h)).isSeparatedFor.ext

Goal state after:
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 := ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ W⦄,
    (B ⋯).arrows f_1 →
      (ConcreteCategory.hom (P.map f_1.op)) (t (h ≫ f) ⋯) =
        (ConcreteCategory.hom (P.map f_1.op)) ((ConcreteCategory.hom (P.map h.op)) (t f hf))
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
F : D ⥤ 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
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ whiskerRight (J.toSheafify P) F ≫ (J.sheafifyCompIso F P).hom = J.toSheafify (P ⋙ F)

Tactic:
dsimp [sheafifyCompIso]

Goal state after:
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), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ whiskerRight (J.toSheafify P) F ≫ (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom =
    J.toSheafify (P ⋙ F)
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by
  suffices Mono f ↔ Mono ((forget TopCat).map f) by
    rw [this, CategoryTheory.mono_iff_injective]
    rfl
  constructor
  · intro
    apply Functor.map_mono -- was `infer_instance`
  · apply Functor.mono_of_mono_map

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

Goal state before:
pp: case h.left
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom (prod.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.left }))
      ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂)) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x

Tactic:
erw [Limits.prod.map_fst]

Goal state after:
case h.left
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom (prod.fst ≫ f)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂)) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ''
      range ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left })) =
    (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ''
        range ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right })))ᶜ

Tactic:
erw [← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr, Set.image_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₂.desc
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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))) → Z ⟶ s.pt

Tactic:
exact fun s => ↾fun x => dite _ (fun h => s.inl <| eX.symm ⟨x, h⟩)
        fun h => s.inr <| eY.symm ⟨x, (this x).resolve_left h⟩

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
⊢ IsVanKampenColimit ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))

Tactic:
apply BinaryCofan.isVanKampen_mk _ _ (fun X Y => TopCat.binaryCofanIsColimit X Y) _
      fun f g => TopCat.pullbackConeIsLimit f g

Goal state after:
case h₁
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
⊢ ∀ {X' Y' : TopCat} (αX : X' ⟶ TopCat.of PUnit.{u + 1}) (αY : Y' ⟶ TopCat.of PUnit.{u + 1})
    (f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt),
    αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f →
      αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f →
        IsPullback (X'.binaryCofan Y').inl αX f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl ∧
          IsPullback (X'.binaryCofan Y').inr αY f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr

case h₂
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
⊢ {Z : TopCat} →
    (f : Z ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt) →
      IsColimit
        (BinaryCofan.mk
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl).fst
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr).fst)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
⊢ H.IsVanKampen

Tactic:
by
  obtain ⟨hc₁⟩ := (is_coprod_iff_isPushout c hc H.1).mpr H
  introv W' hf hg hh hi w
  obtain ⟨hc₂⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
    (BinaryCofan.mk _ (pullback.fst _ _)) _ _ _ hg.w.symm pullback.condition.symm).mpr
    ⟨hg, IsPullback.of_hasPullback αY c.inr⟩
  refine (is_coprod_iff_isPushout _ hc₂ w).symm.trans ?_
  refine ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁)
    (BinaryCofan.mk _ _) (pullback.snd _ _) _ _ ?_ hh.w.symm).trans ?_
  · dsimp; rw [← pullback.condition_assoc, Category.assoc, hi.w]
  constructor
  · rintro ⟨hc₃, hc₄⟩
    refine ⟨hc₄, ?_⟩
    let Y'' := pullback αZ i
    let cmp : Y' ⟶ Y'' := pullback.lift i' αY hi.w
    have e₁ : (g' ≫ cmp) ≫ pullback.snd _ _ = αW ≫ c.inl := by
      rw [Category.assoc, pullback.lift_snd, hg.w]
    have e₂ : (pullback.fst _ _ ≫ cmp : pullback αY c.inr ⟶ _) ≫ pullback.snd _ _ =
        pullback.snd _ _ ≫ c.inr := by
      rw [Category.assoc, pullback.lift_snd, pullback.condition]
    obtain ⟨hc₄⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
      (BinaryCofan.mk _ _) αW _ _ e₁.symm e₂.symm).mpr <| by
        constructor
        · apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]; exact hf.paste_horiz hc₄
        · apply IsPullback.of_right _ e₂ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst]; exact hc₃
    rw [← Category.id_comp αZ, ← show cmp ≫ pullback.snd _ _ = αY from pullback.lift_snd _ _ _]
    apply IsPullback.paste_vert _ (IsPullback.of_hasPullback αZ i)
    have : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom := by
      apply BinaryCofan.IsColimit.hom_ext hc₂
      exacts [(hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.left⟩).symm,
        (hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.right⟩).symm]
    rw [this]
    exact IsPullback.of_vert_isIso ⟨by rw [← this, Category.comp_id, pullback.lift_fst]⟩
  · rintro ⟨hc₃, hc₄⟩
    exact ⟨(IsPullback.of_hasPullback αY c.inr).paste_horiz hc₄, hc₃⟩

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
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
have : IsInitial c.pt := by
    have := (IsColimit.precomposeInvEquiv (Functor.uniqueFromEmpty _) _).symm
      (hc.whiskerEquivalence (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J))
    exact IsColimit.ofIsoColimit this (Cocone.ext (Iso.refl c.pt) (fun {X} ↦ isEmptyElim X))
  replace this := IsInitial.isVanKampenColimit this
  apply (IsVanKampenColimit.whiskerEquivalence_iff
    (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)).mp
  exact (this.precompose_isIso (Functor.uniqueFromEmpty
    ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F)).hom).of_iso
    (Cocone.ext (Iso.refl _) (by simp))

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
⊢ P.isoClosure.isLocal = P.isLocal

Tactic:
ext X Y f

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.isoClosure.isLocal f ↔ P.isLocal f
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
⊢ P.isoClosure.isColocal g → P.isColocal g

Tactic:
intro hg X hX

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isoClosure.isColocal g
X : C
hX : P X
⊢ Function.Bijective fun f ↦ f ≫ g
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₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h ↦ imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h ↦ imageSieve f₁ (Exists.choose h)) ∈ J U✝

Tactic:
apply J.bind_covering

Goal state after:
case hS
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₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h ↦ imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ imageSieve f₂ s ∈ J U✝

case hR
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₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h ↦ imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U✝⦄ (H : (imageSieve f₂ s).arrows f), imageSieve f₁ (Exists.choose H) ∈ J Y
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 (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)) x)

Tactic:
← h₁,

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 (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)) x)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst✝ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
hf : Sieve.ofArrows X f ∈ J S
U : C
u : ToType ((shrinkYoneda.{w, v, u}.obj S).obj (op U))
⊢ Presheaf.imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)) u ∈ J U

Tactic:
obtain ⟨u, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective u
    replace hf := J.pullback_stable u hf
    rwa [← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc u] at hf

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (initial.to ((Discrete.functor f).obj i)) (initial.to ((Discrete.functor f).obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
this : ∀ (i : Discrete ι), Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i)
⊢ IsPullback (initial.to ((Discrete.functor f).obj i)) (initial.to ((Discrete.functor f).obj j)) (c.ι.app i) (c.ι.app j)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext X Y i)

Tactic:
have : Subsingleton (Ext X Y i) := ⟨fun e₁ e₂ ↦ by simp only [hX i hi]⟩
    let := HasExt.standard C
    exact Ext.chgUniv.{max u v, w}.symm.subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (mapComp (f ≫ g) h).hom ≫
        (mapComp f g).hom ▷ map h ≫
          (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
      eqToHom ⋯
map₂_left_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ : B
f✝ g✝ : a✝ ⟶ b✝
φ : f✝ ⟶ g✝
⊢ map f✝ = map g✝

Tactic:
obtain rfl := obj_ext_of_isDiscrete φ

Goal state after:
B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (mapComp (f ≫ g) h).hom ≫
        (mapComp f g).hom ▷ map h ≫
          (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
      eqToHom ⋯
map₂_left_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ : B
f✝ : a✝ ⟶ b✝
φ : f✝ ⟶ f✝
⊢ map f✝ = map f✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ : B
f✝ g✝ : a✝ ⟶ b✝
φ : f✝ ⟶ g✝
⊢ map f✝ = map g✝

Tactic:
obtain rfl := obj_ext_of_isDiscrete φ

Goal state after:
B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ : B
f✝ : a✝ ⟶ b✝
φ : f✝ ⟶ f✝
⊢ map f✝ = map f✝
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
· cases g
      apply BiconeHom.right

Goal state after:
case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)

Tactic:
· intro Z g hg
    change _ ∈ J₁ _
    rw [← Sieve.pullback_comp]
    apply hg

Goal state after: