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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ ((F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                    ⋯).hom.toNatTrans.app
            M ≫
          (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
            (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                      ⋯).inv.toNatTrans.app
              N) ≫
      (F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).hom.toNatTrans.app N =
    (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          (((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M ≫ g) ≫
            (F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).hom.toNatTrans.app N) ≫
        (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).inv.toNatTrans.app
          ((F.map q.op.toLoc).toFunctor.obj N)

Tactic:
simp only [Category.assoc,
        Functor.map_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ (F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).inv.toNatTrans.app M ≫
      (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                  ⋯).hom.toNatTrans.app
          M ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                      ⋯).inv.toNatTrans.app
              N ≫
            (F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).hom.toNatTrans.app N =
    (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
              ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).hom.toNatTrans.app N) ≫
            (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).inv.toNatTrans.app
              ((F.map q.op.toLoc).toFunctor.obj N)
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsStackFor R.arrows
S✝ : C
R : Sieve S✝
hR : R ∈ J S✝
this : (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
⊢ (F.toDescentData fun f ↦ f.obj.hom).EssSurj

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this✝¹ :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
Z : Over (X i)
Y : C
j : ι'
p : Z.left ⟶ X' j
ψ : D₁ ⟶ D₂
hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom ⋯) ≫ f i
this✝ : Over.Hom.left (Over.homMk Z.hom ⋯) = Z.hom
this :
  (F.map Z.hom.op.toLoc).toFunctor.map (ψ.hom i) ≫ D₂.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫ (F.map ((p' j).op.toLoc ≫ p.op.toLoc)).toFunctor.map (ψ.hom (α j))
⊢ (F.mapComp' (𝟙 { as := op (X i) }) Z.hom.op.toLoc Z.hom.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i) ≫
      (F.map Z.hom.op.toLoc).toFunctor.map
          ((F.mapId { as := op (X i) }).hom.toNatTrans.app (D₁.obj i) ≫
            ψ.hom i ≫ (F.mapId { as := op (X i) }).inv.toNatTrans.app (D₂.obj i)) ≫
        (F.mapComp' (𝟙 { as := op (X i) }) Z.hom.op.toLoc Z.hom.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i) =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      ((F.mapComp' (p' j).op.toLoc p.op.toLoc ((p' j).op.toLoc ≫ p.op.toLoc) ⋯).hom.toNatTrans.app (D₁.obj (α j)) ≫
          (F.map p.op.toLoc).toFunctor.map ((F.map (p' j).op.toLoc).toFunctor.map (ψ.hom (α j))) ≫
            (F.mapComp' (p' j).op.toLoc p.op.toLoc ((p' j).op.toLoc ≫ p.op.toLoc) ⋯).inv.toNatTrans.app
              (D₂.obj (α j))) ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯

Tactic:
simp [mapComp'_inv_naturality, Cat.Hom.comp_toFunctor,
        Functor.comp_obj, Cat.Hom.hom_inv_id_toNatTrans_app_assoc, ← reassoc_of% this,
        D₂.hom_self _ _ rfl, F.mapComp'_id_comp_inv_app, ← Functor.map_comp,
        F.mapComp'_id_comp_hom_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (pullback.fst fst (𝒰.f i)) (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯)
    (pullback.lift fst snd h) m
heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) = H'.isoPullback.inv ≫ ⋯.isoPullback.hom
⊢ IsIso (H'.isoPullback.inv ≫ ⋯.isoPullback.hom)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
⊢ ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
    ↾(Over.map (f ≫ g).unop).op.whiskerLeft = ↾(Over.map f.unop).op.whiskerLeft ≫ ↾(Over.map g.unop).op.whiskerLeft

Tactic:
by
    rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ ⟨f : Y ⟶ X⟩ ⟨g : Z ⟶ Y⟩
    ext φ ⟨W⟩
    simpa [Over.mapComp] using φ.naturality ((Over.mapComp g f).hom.app W).op

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

Goal state before:
pp: case left.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac
            simpa using s.condition =≫ F.obj.map φ.op

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

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd) ⋯

Tactic:
apply F.2.hom_ext_ofArrows _ h₂

Goal state after:
case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ ∀ (i : WalkingPair),
    m ≫ F.obj.map (WalkingPair.casesOn i sq.f₂₄ sq.f₃₄).op =
      ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
          ⋯ ≫
        F.obj.map (WalkingPair.casesOn i sq.f₂₄ sq.f₃₄).op
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Tactic:
by
  have := (S.toSquare.op.map P).pullbackCone.isLimitEquivBijective
  exact ⟨fun h ↦ this h.isLimit, fun h ↦ Square.IsPullback.mk _ (this.symm h)⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
inst✝ : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
⊢ Mono (-(presheafToSheaf J AddCommGrpCat).map (Functor.whiskerRight (yoneda.map S.f₁₃) AddCommGrpCat.free))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
inst✝⁶ : MonoidalCategory A
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
inst✝⁴ : G.IsCoverDense J
inst✝³ : G.Full
inst✝² : G.IsContinuous K J
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.W.IsMonoidal
⊢ (K.W.inverseImage ((Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op)).IsMonoidal

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
⊢ Function.Bijective fun g_1 ↦ F ◁ g ≫ g_1

Tactic:
have := hg _ (Presheaf.isSheaf_functorEnrichedHom F H h)
  rw [← Function.Bijective.of_comp_iff' (f := MonoidalClosed.curry)
    ((ihom.adjunction _).homEquiv _ _).bijective]
  rw [← Function.Bijective.of_comp_iff (g := MonoidalClosed.curry) _
    ((ihom.adjunction _).homEquiv _ _).bijective] at this
  convert! this using 1
  ext α : 1
  dsimp
  rw [curry_natural_left]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows

Tactic:
exact presheafHom_isSheafFor F G S
    (fun _ _ => ((Presheaf.isSheaf_iff_isLimit J G).1 hG _ (J.pullback_stable _ hS)).some)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
inst✝¹² : LocallySmall.{w, v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝¹¹ : Category.{v', u'} A
inst✝¹⁰ : MonoidalCategory A
inst✝⁹ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁸ : HasProducts A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁷ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁶ : ConcreteCategory A FC
inst✝⁵ : HasWeakSheafify J A
inst✝⁴ : (forget A).ReflectsIsomorphisms
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝² : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝¹ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst✝ : J.HasSheafCompose (forget A)
X₁✝ X₂✝ Y₁✝ Y₂✝ : Cᵒᵖ ⥤ A
f : X₁✝ ⟶ X₂✝
g : Y₁✝ ⟶ Y₂✝
hf : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)
hg : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map g)
Φ : P.FullSubcategory
⊢ IsIso
    (Functor.OplaxMonoidal.δ Φ.obj.presheafFiber X₁✝ Y₁✝ ≫
      (Φ.obj.presheafFiber.map f ⊗ₘ Φ.obj.presheafFiber.map g) ≫ Functor.LaxMonoidal.μ Φ.obj.presheafFiber X₂✝ Y₂✝)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
N : Type u'
inst✝¹ : Category.{v', u'} N
p : N ⥤ C
inst✝ : InitiallySmall N
U V : N
g : V ⟶ U
⊢ fiberMk (p.map g) = fiberMk (𝟙 (p.obj U))

Tactic:
by
  simpa using fiberMk_map_comp (p := p) g (𝟙 (p.obj U))

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, u} C
⊢ ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} (ObjectProperty.ofObj pointBot)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, u} C
⊢ ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} (pointsBot C)

Tactic:
by
  dsimp [pointsBot]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
V U : N
f : p.obj U ⟶ X
φ₁ : ((functor p).obj V).fst ⟶ ⟨X, fiberMk f⟩.fst
hφ₁ : (hom ((fiber p).map φ₁)) ((functor p).obj V).snd = ⟨X, fiberMk f⟩.snd
φ₂ : ((functor p).obj V).fst ⟶ ⟨X, fiberMk f⟩.fst
hφ₂ : (hom ((fiber p).map φ₂)) ((functor p).obj V).snd = ⟨X, fiberMk f⟩.snd
⊢ fiberMk φ₁ = fiberMk φ₂

Tactic:
simpa using hφ₁.trans hφ₂.symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_3
k : ι''
⊢ q' k ≫ f' (β k) ≫ p = f'' k ≫ r

Tactic:
reassoc_of% w',

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_3
k : ι''
⊢ f'' k ≫ q ≫ p = f'' k ≫ r
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
X : C
R : Presieve X
h : R ∈ K.coverings X
h' : Presieve.IsSheafFor F R
⊢ Presieve.IsSheafFor (K.subsheafify 𝒮).toFunctor R

Tactic:
let G := K.subsheafify 𝒮
  rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
  refine ⟨.of_mono G.ι h'.isSeparatedFor, fun x hx ↦ ?_⟩
  obtain ⟨t, ht, uniq⟩ := h' (x.map G.ι) (hx.map G.ι)
  exact ⟨⟨t, .amalgamate h (hx.map G.ι) (fun _ _ hr ↦ (x _ hr).property) ht⟩, .of_mono _ ht⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
ht₂

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
⊢ Epi ((sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝² : Epi ((presheafToSheaf J D).map f.hom)
this✝¹ : Epi ((presheafToSheaf J D).map i)
this✝ : IsIso ((presheafToSheaf J D).map i)
this : EffectiveEpi ((presheafToSheaf J D).map f.hom)
⊢ EffectiveEpi
    (inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝² : Epi ((presheafToSheaf J D).map f.hom)
this✝¹ : Epi ((presheafToSheaf J D).map i)
this✝ : IsIso ((presheafToSheaf J D).map i)
this : EffectiveEpi ((presheafToSheaf J D).map p)
⊢ EffectiveEpi ((presheafToSheaf J D).map p ≫ (presheafToSheaf J D).map i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve S
h : F.IsStackFor R
this : (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
⊢ (F.toDescentData fun f ↦ f.obj.hom).EssSurj

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ (associativity C D E).functor.IsEquivalence

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ (associativity C D E).inverse.IsEquivalence

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

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
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ unop ((triangleOpEquivalence D).inverse.obj ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T)))) ∈
    Pretriangulated.distinguishedTriangles

Tactic:
← mem_distTriang_op_iff,

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ (triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T)) ∈ Pretriangulated.distinguishedTriangles