awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_3 : Category.{w', w} A
inst_4 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_5 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
inst :
  ∀ (X : Aᵒᵖ),
    IsIso (X :=
      obj
        (obj yoneda
          ((obj (sheafToPresheaf J A)
                (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
            (op U)))
        X)
      (NatTrans.app
        (map yoneda
          (NatTrans.app
            (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
            (op U)))
        X)
⊢ IsIso (X :=
    obj yoneda
      ((obj (sheafToPresheaf J A)
            (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
        (op U)))
    (map yoneda
      (NatTrans.app
        (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y)) (op U)))

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
⊢ IsIso (X :=
    obj
      (obj yoneda
        ((obj (sheafToPresheaf J A)
              (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
          (op U)))
      (op X))
    (NatTrans.app
      (map yoneda
        (NatTrans.app
          (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
          (op U)))
      (op X))

Tactic:
simpa [sheafAdjunctionCocontinuous_counit_app_hom]
    using isIso_ranCounit_app_of_isDenseSubsite G J K Y U X

Premises used: CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom, CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
⊢ IsEquivalence (C := Sheaf.{v_2, w', u_2, w} K A) (G.sheafPushforwardContinuous A J K)

Tactic:
(G.sheafAdjunctionCocontinuous A J K).toEquivalence.isEquivalence_functor

Premises used: CategoryTheory.Functor.sheafAdjunctionCocontinuous, CategoryTheory.ObjectProperty.lift, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Functor.sheafPushforwardContinuous, CategoryTheory.Adjunction.toEquivalence
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ IsIso (D.hom q f₁ f₂ hf₁ hf₂)

Tactic:
(D.iso q f₁ f₂).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Pseudofunctor.DescentData.iso
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
h : ∀ (i : ι), φ.hom i = φ'.hom i
⊢ φ = φ'

Tactic:
Hom.ext (funext h)

Premises used: funext, CategoryTheory.Pseudofunctor.DescentData.Hom.ext
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
i : ι
⊢ Hom.hom (𝟙 D) i = 𝟙 (D.obj i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ D₃ : F.DescentData f
φ : D₁ ⟶ D₂
φ' : D₂ ⟶ D₃
i : ι
⊢ (φ ≫ φ').hom i = φ.hom i ≫ φ'.hom i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X i₁) }) (f i₁).op.toLoc f₁.op.toLoc) q.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X i₂) }) (f i₂).op.toLoc f₂.op.toLoc) q.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X i₁) }) (f i₁).op.toLoc f₁.op.toLoc) q.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op Y }) f₁.op.toLoc g.op.toLoc) gf₁.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op (X i₁) }) (f i₁).op.toLoc gf₁.op.toLoc) q'.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X i₂) }) (f i₂).op.toLoc f₂.op.toLoc) q.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op Y }) f₂.op.toLoc g.op.toLoc) gf₂.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op Y }) q.op.toLoc g.op.toLoc) q'.op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ pullHom
      ((F.mapComp' (f i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' (f i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app M)
      g gf₁ gf₂ ⋯ ⋯ =
    (F.mapComp' (f i₁).op.toLoc gf₁.op.toLoc q'.op.toLoc ⋯).inv.toNatTrans.app M ≫
      (F.mapComp' (f i₂).op.toLoc gf₂.op.toLoc q'.op.toLoc ⋯).hom.toNatTrans.app M

Tactic:
simp only [pullHom, Functor.map_comp, Category.assoc,
      F.mapComp'₀₁₃_inv_app (f i₁).op.toLoc f₁.op.toLoc g.op.toLoc q.op.toLoc
        gf₁.op.toLoc q'.op.toLoc (by grind) (by grind) (by grind),
      F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app (f i₂).op.toLoc f₂.op.toLoc g.op.toLoc
      q.op.toLoc gf₂.op.toLoc q'.op.toLoc (by grind) (by grind) (by grind)]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, Quiver.Hom.toLoc, CategoryTheory.Functor.map_comp, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (f₁ ≫ p' j₁) ≫ f (α j₁) = q ≫ p

Tactic:
simp [w, reassoc_of% hf₁]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (f₂ ≫ p' j₂) ≫ f (α j₂) = q ≫ p

Tactic:
simp [w, reassoc_of% hf₂]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : autoParam (f₁ ≫ f' j₁ = q) pullFunctorObjHom_eq._auto_1
hf₂ : autoParam (f₂ ≫ f' j₂ = q) pullFunctorObjHom_eq._auto_2
hq' : autoParam (q ≫ p = q') pullFunctorObjHom_eq._auto_3
hf₁' : autoParam (f₁ ≫ p' j₁ = f₁') pullFunctorObjHom_eq._auto_4
hf₂' : autoParam (f₂ ≫ p' j₂ = f₂') pullFunctorObjHom_eq._auto_5
rw : f₁' ≫ f (α j₁) = q ≫ p
rw₁ : (f₁ ≫ p' j₁) ≫ f (α j₁) = q ≫ p
rw₂ : f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p
rw₃ : f₁ ≫ f' j₁ ≫ p = q ≫ p
rw₄ rw₅ : q ≫ p = q ≫ p
⊢ f₁' ≫ f (α j₁) = q'

Tactic:
rw [← hq', ← hf₁', Category.assoc, w, reassoc_of% hf₁]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : autoParam (f₁ ≫ f' j₁ = q) pullFunctorObjHom_eq._auto_1
hf₂ : autoParam (f₂ ≫ f' j₂ = q) pullFunctorObjHom_eq._auto_2
hq' : autoParam (q ≫ p = q') pullFunctorObjHom_eq._auto_3
hf₁' : autoParam (f₁ ≫ p' j₁ = f₁') pullFunctorObjHom_eq._auto_4
hf₂' : autoParam (f₂ ≫ p' j₂ = f₂') pullFunctorObjHom_eq._auto_5
rw : f₂' ≫ f (α j₂) = q ≫ p
rw₁ : (f₂ ≫ p' j₂) ≫ f (α j₂) = q ≫ p
rw₂ : f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p
rw₃ : f₂ ≫ f' j₂ ≫ p = q ≫ p
rw₄ rw₅ : q ≫ p = q ≫ p
⊢ f₂' ≫ f (α j₂) = q'

Tactic:
rw [← hq', ← hf₂', Category.assoc, w, reassoc_of% hf₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
hq' : q ≫ p = q'
hf₁' : f₁ ≫ p' j₁ = f₁'
hf₂' : f₂ ≫ p' j₂ = f₂'
subst :
  pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))
⊢ pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom q' f₁' f₂' ⋯ ⋯ ≫ (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))

Tactic:
subst hq' hf₁' hf₂'
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))

Tactic:
simp [mapComp'_eq_mapComp, pullFunctorObjHom]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_eq_mapComp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
rw :
  pullHom
      ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂)))
      g gf₁ gf₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc (gf₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q' ≫ p) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc (gf₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))
⊢ pullHom (pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ = pullFunctorObjHom w D (gf₁ ≫ f' j₁) gf₁ gf₂ ⋯ ⋯

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ (q' ≫ p) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)]

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
rw rw₁ : q' ≫ p = q' ≫ p
⊢ g ≫ q ≫ p = q' ≫ p

Tactic:
rw [reassoc_of% hq]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
rw : f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p
rw₁ : f₁ ≫ f' j₁ ≫ p = q ≫ p
rw₂ rw₃ : q ≫ p = q ≫ p
⊢ (f₁ ≫ p' j₁) ≫ f (α j₁) = q ≫ p

Tactic:
rw [Category.assoc, w, reassoc_of% hf₁]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
rw : f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p
rw₁ : f₂ ≫ f' j₂ ≫ p = q ≫ p
rw₂ rw₃ : q ≫ p = q ≫ p
⊢ (f₂ ≫ p' j₂) ≫ f (α j₂) = q ≫ p

Tactic:
rw [Category.assoc, w, reassoc_of% hf₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
rw :
  pullHom
      ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂)))
      g gf₁ gf₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc (gf₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      pullHom (D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯) g (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc (gf₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))
⊢ pullHom
      ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂)))
      g gf₁ gf₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc (gf₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q' ≫ p) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc (gf₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))

Tactic:
rw [← D.pullHom_hom g (q ≫ p) (q' ≫ p) (by rw [reassoc_of% hq])
      (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) (by rw [Category.assoc, w, reassoc_of% hf₁])
      (by rw [Category.assoc, w, reassoc_of% hf₂]) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂)
      (by cat_disch) (by cat_disch)]

Premises used: CategoryTheory.Pseudofunctor.DescentData.pullHom_hom, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq.{v + 1} (α := { as := op (X (α j₁)) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op (X' j₁) }) (p' j₁).op.toLoc gf₁.op.toLoc)
    (CategoryStruct.comp (Y := { as := op (X' j₁) }) (p' j₁).op.toLoc gf₁.op.toLoc)
⊢ Eq.{v + 1} (α := { as := op (X (α j₁)) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op (X' j₁) }) (p' j₁).op.toLoc gf₁.op.toLoc)
    (CategoryStruct.comp (Y := { as := op (X' j₁) }) (p' j₁).op.toLoc gf₁.op.toLoc)

Tactic:
cat_disch