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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ presheafObjπ data G₀ Y✝ i ≫ IsDenseSubsite.mapPreimage J F G₀ p =
    presheafObjπ data G₀ Y✝ i ≫ IsDenseSubsite.mapPreimage J F G₀ p

pp: case fac
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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ p ≫ (data Y✝).f i = F.map (b ≫ (data X).p₂ j) ≫ (data X).f i₂ ≫ f

pp: case fac
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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ p ≫ (data Y✝).f i = F.map (b ≫ (data X).p₁ j) ≫ (data X).f i₁ ≫ f

Tactic:
]

Goal state after:
case fac
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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ p ≫ (data Y✝).f i = F.map (b ≫ (data X).p₂ j) ≫ (data X).f i₂ ≫ f

case fac
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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ p ≫ (data Y✝).f i = F.map (b ≫ (data X).p₁ j) ≫ (data X).f i₁ ≫ f