mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres✝ : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
i : Sigma κ
t : ↑(PrimeSpectrum.basicOpen (a i.fst i.snd)) ⟶ ↑(U ↑i.fst) := (Spec R).homOfLE ⋯
iso : restrictFunctor (U ↑i.fst).ι ⋙ restrictFunctor ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) ≅
  restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd))))) :=
  (restrictFunctorComp ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (U ↑i.fst).ι).symm ≪≫ restrictFunctorCongr ⋯
pres : SheafOfModules.Presentation
  ((restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))).obj M) :=
  SheafOfModules.Presentation.ofIsIso (iso.app M).hom
    (presentationRestrict ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (pres✝ ↑i.fst))
this : Aux (M.restrict (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))) ⊤
⊢ Aux M (PrimeSpectrum.basicOpen (a i.fst i.snd))

Tactic:
]

Goal state after:
case refine_2
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres✝ : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
i : Sigma κ
t : ↑(PrimeSpectrum.basicOpen (a i.fst i.snd)) ⟶ ↑(U ↑i.fst) := (Spec R).homOfLE ⋯
iso : restrictFunctor (U ↑i.fst).ι ⋙ restrictFunctor ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) ≅
  restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd))))) :=
  (restrictFunctorComp ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (U ↑i.fst).ι).symm ≪≫ restrictFunctorCongr ⋯
pres : SheafOfModules.Presentation
  ((restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))).obj M) :=
  SheafOfModules.Presentation.ofIsIso (iso.app M).hom
    (presentationRestrict ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (pres✝ ↑i.fst))
this : Aux (M.restrict (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))) ⊤
⊢ Aux M (PrimeSpectrum.basicOpen (a i.fst i.snd))
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
⊢ (↑S).arrows (F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁)

Tactic:
]

Goal state after:
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
⊢ (↑S).arrows (F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁)
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } =
    s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ }

Tactic:
]

Goal state after:
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } =
    s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ }
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case e_6
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂ = F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂

Tactic:
]

Goal state after:
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S).arrows (F.map d ≫ F.map b ≫ (data a.Y).f i ≫ a.f)

Tactic:
]

Goal state after:
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S).arrows (F.map d ≫ F.map b ≫ (data a.Y).f i ≫ a.f)
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ s.ι { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he } = s.ι a ≫ G.map (F.map d ≫ F.map b ≫ (data a.Y).f i).op

Tactic:
]

Goal state after:
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ s.ι { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he } = s.ι a ≫ G.map (F.map d ≫ F.map b ≫ (data a.Y).f i).op
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
G : Cᵒᵖ ⥤ A
x✝ : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))

Tactic:
]

Goal state after:
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
G : Cᵒᵖ ⥤ A
x✝ : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (Opposite.op T)
F : Sheaf J D
⊢ IsConstant J F ↔ (constantSheaf J D).essImage F

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (Opposite.op T)
F : Sheaf J D
⊢ IsConstant J F ↔ (constantSheaf J D).essImage F
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasWeakSheafify J D
inst✝² : (constantSheaf J D).Faithful
inst✝¹ : (constantSheaf J D).Full
F : Sheaf J D
inst✝ : IsConstant J F
T : C
hT : IsTerminal T
⊢ (constantSheaf J D).essImage F

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasWeakSheafify J D
inst✝² : (constantSheaf J D).Faithful
inst✝¹ : (constantSheaf J D).Full
F : Sheaf J D
inst✝ : IsConstant J F
T : C
hT : IsTerminal T
⊢ (constantSheaf J D).essImage F
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ sheafifyMap J (constComp Cᵒᵖ (F.obj.obj (Opposite.op T)) U).hom ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).hom =
    (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)))).hom ≫
      whiskerRight ((constantSheafAdj J D hT).counit.app F).hom U

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ sheafifyMap J (constComp Cᵒᵖ (F.obj.obj (Opposite.op T)) U).hom ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).hom =
    (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)))).hom ≫
      whiskerRight ((constantSheafAdj J D hT).counit.app F).hom U
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsIso
    ((constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T)) ≫
      (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F))

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsIso
    ((constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T)) ≫
      (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F))
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsConstant J F

Tactic:
have : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)) := by
    rw [← constantSheafAdj_counit_w]
    infer_instance

Goal state after:
C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsConstant J F
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsIso ((constantSheafAdj J D hT).counit.app F)

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsIso ((constantSheafAdj J D hT).counit.app F)
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 : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map a ≫ F.map g ≫ f = F.map a ≫ F.map g ≫ f

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E : PreZeroHypercover X
h : ∃ E_1, P.property E_1 ∧ E.presieve₀ = E_1.presieve₀
⊢ P.property E

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E : PreZeroHypercover X
h : ∃ E_1, P.property E_1 ∧ E.presieve₀ = E_1.presieve₀
⊢ P.property E
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
⊢ P.property E.shrink

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
⊢ P.property E.shrink
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
⊢ P.property F.shrink

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
⊢ P.property F.shrink
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [IsIso f], P.property (PreZeroHypercover.singleton f)
S T : C
f : S ⟶ T
hf : IsIso f
⊢ (PreZeroHypercover.singleton f).presieve₀ ∈ P.precoverage.coverings T

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [IsIso f], P.property (PreZeroHypercover.singleton f)
S T : C
f : S ⟶ T
hf : IsIso f
⊢ (PreZeroHypercover.singleton f).presieve₀ ∈ P.precoverage.coverings T
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h₁ : ∀ {X : C}, P.property.IsClosedUnderIsomorphisms
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
e : F ≅ PreZeroHypercover.pullback₁ g E := PreZeroHypercover.isoMk (Equiv.refl F.I₀) (fun i ↦ ⋯.isoPullback) ⋯
⊢ P.property (PreZeroHypercover.pullback₁ g E)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h₁ : ∀ {X : C}, P.property.IsClosedUnderIsomorphisms
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
e : F ≅ PreZeroHypercover.pullback₁ g E := PreZeroHypercover.isoMk (Equiv.refl F.I₀) (fun i ↦ ⋯.isoPullback) ⋯
⊢ P.property (PreZeroHypercover.pullback₁ g E)