mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
⊢ f ≫ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ = 𝟙 X

pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
⊢ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ ≫ f = 𝟙 Y

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
⊢ f ≫ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ = 𝟙 X
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
⊢ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ ≫ f = 𝟙 Y

Tactic:
·

Goal state after:
case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
⊢ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ ≫ f = 𝟙 Y
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) ≫ pullback.fst f g =
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.fst f g

Tactic:
simp [m, pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) ≫ pullback.snd f g =
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.snd f g

Tactic:
simp [m, pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ f.hom.app W ≫ invMap = 𝟙 (F.obj.obj W)

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ invMap ≫ f.hom.app W = 𝟙 (G.obj.obj W)

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ f.hom.app W ≫ invMap = 𝟙 (F.obj.obj W)
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ invMap ≫ f.hom.app W = 𝟙 (G.obj.obj W)

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ invMap ≫ f.hom.app W = 𝟙 (G.obj.obj W)
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ x.IsAmalgamation y →
    ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ (∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))) →
    x.IsAmalgamation y

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ x.IsAmalgamation y →
    ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ (∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))) →
    x.IsAmalgamation y

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ (∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))) →
    x.IsAmalgamation y
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case left.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op

pp: case right.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map b.op

pp: case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op

Tactic:
·

Goal state after:
case left.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case right.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map b.op

pp: case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op

Tactic:
·

Goal state after:
case right.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map b.op
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op

Tactic:
have H' := (x (Z₁.hom ≫ g) hZ₁).naturality φ.op

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  ((Over.forget (unop (op Z₁.left))).op ⋙ F).map φ.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ ((Over.forget (unop (op Z₁.left))).op ⋙ G).map φ.op
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op

Tactic:
·

Goal state after:
case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ (pullFunctor F ⋯).FullyFaithful

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ Nonempty (F.toDescentData f ⋙ pullFunctor F ⋯ ≅ F.toDescentData f')

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ (pullFunctor F ⋯).FullyFaithful
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ Nonempty (F.toDescentData f ⋙ pullFunctor F ⋯ ≅ F.toDescentData f')

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ Nonempty (F.toDescentData f ⋙ pullFunctor F ⋯ ≅ F.toDescentData f')
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x✝ : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
⊢ ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j x✝.fst x✝.snd)
        ⋯ ≫
      (sq.op.map F.obj).f₁₂ =
    x✝.fst

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x✝ : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
⊢ ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j x✝.fst x✝.snd)
        ⋯ ≫
      (sq.op.map F.obj).f₁₃ =
    x✝.snd

pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd) ⋯

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x✝ : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
⊢ ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j x✝.fst x✝.snd)
        ⋯ ≫
      (sq.op.map F.obj).f₁₂ =
    x✝.fst
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x✝ : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
⊢ ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j x✝.fst x✝.snd)
        ⋯ ≫
      (sq.op.map F.obj).f₁₃ =
    x✝.snd

pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd) ⋯

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
x✝ : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
⊢ ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j x✝.fst x✝.snd)
        ⋯ ≫
      (sq.op.map F.obj).f₁₃ =
    x✝.snd