Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case left.left.id
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
i₁ : data.multicospanShape.L
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁)) ≫
      match WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁))

pp: case left.right.fst
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.fst j₂) ≫
      match WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left (data.multicospanShape.fst j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.fst j₂)

pp: case left.right.snd
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.snd j₂) ≫
      match WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left (data.multicospanShape.snd j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.snd j₂)

pp: case right.right.id
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₁ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁)) ≫
      match WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁))

Tactic:
<;>

Goal state after:
case left.left.id
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
i₁ : data.multicospanShape.L
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁)) ≫
      match WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁))

case left.right.fst
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.fst j₂) ≫
      match WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left (data.multicospanShape.fst j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.fst j₂)

case left.right.snd
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.snd j₂) ≫
      match WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left (data.multicospanShape.snd j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.snd j₂)

case right.right.id
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₁ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁)) ≫
      match WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁))