Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: 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
⊢ ∀ ⦃X_1 Y : WalkingMulticospan data.multicospanShape⦄ (f_1 : X_1 ⟶ Y),
    ((data.multicospanIndex P).multicospan.map f_1 ≫
        match Y with
        | WalkingMulticospan.left i => f.app (op (data.X i))
        | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
      (match X_1 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 f_1

Tactic:
rintro (i₁ | j₁) (i₂ | j₂) (_ | _)

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₁))