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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
        ((F.map (p' (β k₁)).op.toLoc).toFunctor.obj (D.obj (α (β k₁)))) ≫
      (F.mapComp' (p' (β k₁)).op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ((r' k₁).op.toLoc ≫ f₁.op.toLoc)
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁))) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (r' k₂).op.toLoc f₂.op.toLoc ((r' k₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D.obj (α (β k₂))) =
    (F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
        ((F.map (p' (β k₁)).op.toLoc).toFunctor.obj (D.obj (α (β k₁)))) ≫
      (F.mapComp' (p' (β k₁)).op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ((r' k₁).op.toLoc ≫ f₁.op.toLoc)
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁))) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (p' (β k₂)).op.toLoc ((q' k₂).op.toLoc ≫ f₂.op.toLoc) ((r' k₂).op.toLoc ≫ f₂.op.toLoc)
                      ⋯).hom.toNatTrans.app
              (D.obj (α (β k₂))) ≫
            (F.mapComp' (q' k₂).op.toLoc f₂.op.toLoc ((q' k₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
                ((F.map (p' (β k₂)).op.toLoc).toFunctor.obj (D.obj (α (β k₂)))) ≫
              (F.map f₂.op.toLoc).toFunctor.map
                ((F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯).inv.toNatTrans.app
                  (D.obj (α (β k₂))))

Tactic:
mapComp'₀₂₃_hom_app _ _ _ _ _ _ _ _ rfl rfl

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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
        ((F.map (p' (β k₁)).op.toLoc).toFunctor.obj (D.obj (α (β k₁)))) ≫
      (F.mapComp' (p' (β k₁)).op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ((r' k₁).op.toLoc ≫ f₁.op.toLoc)
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁))) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' ?m.381 (?m.382 ≫ f₂.op.toLoc) ((r' k₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
              (D.obj (α (β k₂))) ≫
            (F.mapComp' ?m.382 f₂.op.toLoc (?m.382 ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
                ((F.map ?m.381).toFunctor.obj (D.obj (α (β k₂)))) ≫
              (F.map f₂.op.toLoc).toFunctor.map
                ((F.mapComp' ?m.381 ?m.382 (r' k₂).op.toLoc ?m.387).inv.toNatTrans.app (D.obj (α (β k₂)))) =
    (F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
        ((F.map (p' (β k₁)).op.toLoc).toFunctor.obj (D.obj (α (β k₁)))) ≫
      (F.mapComp' (p' (β k₁)).op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ((r' k₁).op.toLoc ≫ f₁.op.toLoc)
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁))) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (p' (β k₂)).op.toLoc ((q' k₂).op.toLoc ≫ f₂.op.toLoc) ((r' k₂).op.toLoc ≫ f₂.op.toLoc)
                      ⋯).hom.toNatTrans.app
              (D.obj (α (β k₂))) ≫
            (F.mapComp' (q' k₂).op.toLoc f₂.op.toLoc ((q' k₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
                ((F.map (p' (β k₂)).op.toLoc).toFunctor.obj (D.obj (α (β k₂)))) ≫
              (F.map f₂.op.toLoc).toFunctor.map
                ((F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯).inv.toNatTrans.app
                  (D.obj (α (β k₂))))

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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ LocallyDiscrete Cᵒᵖ

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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ { as := op (X (α (β k₂))) } ⟶ ?m.378

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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ ?m.378 ⟶ { as := op (X'' k₂) }

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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ ?m.381 ≫ ?m.382 = (r' k₂).op.toLoc