mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F : Cᵒᵖ ⥤ A
g : M ⟶ F.obj (op X)
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ∀ (b : (yoneda.obj X).obj x✝²),
    (Sigma.ι (fun i ↦ M) b ≫ (freeYoneda X M).map x✝ ≫ Sigma.desc fun φ ↦ g ≫ F.map (Quiver.Hom.op φ)) =
      Sigma.ι (fun i ↦ M) b ≫ (Sigma.desc fun φ ↦ g ≫ F.map (Quiver.Hom.op φ)) ≫ F.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F : Cᵒᵖ ⥤ A
f : freeYoneda X M ⟶ F
⊢ (fun g ↦ { app := fun Y ↦ Sigma.desc fun φ ↦ g ≫ F.map (Quiver.Hom.op φ), naturality := ⋯ })
      ((fun f ↦ Sigma.ι (fun i ↦ M) (𝟙 (unop (op X))) ≫ f.app (op X)) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F : Cᵒᵖ ⥤ A
g : M ⟶ F.obj (op X)
⊢ (fun f ↦ Sigma.ι (fun i ↦ M) (𝟙 (unop (op X))) ≫ f.app (op X))
      ((fun g ↦ { app := fun Y ↦ Sigma.desc fun φ ↦ g ≫ F.map (Quiver.Hom.op φ), naturality := ⋯ }) g) =
    g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
α : freeYoneda X M ⟶ F
f : F ⟶ G
⊢ freeYonedaHomEquiv (α ≫ f) = freeYonedaHomEquiv α ≫ f.app (op X)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
⊢ SheafOfModules.IsQuasicoherent M ↔ IsIso M.fromTildeΓ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
α : M ⟶ F.obj (op X)
f : F ⟶ G
⊢ freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
N : ModuleCat ↑R
e : (tilde.functor R).obj N ≅ M
⊢ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf ((tilde.functor R).obj N)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
⊢ (ObjectProperty.ofObj fun x ↦
      match x with
      | (X, i) => freeYoneda X (S i)).IsSeparating

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasCoproducts A
inst✝² : HasSeparator A
inst✝¹ : HasZeroMorphisms A
inst✝ : HasCoproducts A
⊢ (ObjectProperty.ofObj fun x ↦ separator A).IsSeparating

Tactic:
by

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)
⊢ ∀ (b : (data X).toOneHypercover.multicospanShape.R),
    liftAux hG₀ s ((data X).toOneHypercover.multicospanShape.fst b) ≫
        ((data X).toOneHypercover.multicospanIndex G).fst b =
      liftAux hG₀ s ((data X).toOneHypercover.multicospanShape.snd b) ≫
        ((data X).toOneHypercover.multicospanIndex G).snd b

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
⊢ (tilde.functor R).essImage = SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M x✝ : ModuleCat ↑R
⊢ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf ((tilde.functor R).obj x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Sheaf

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
⊢ (ObjectProperty.ofObj fun x ↦
      match x with
      | (X, i) => freeYoneda J X (S i)).IsSeparating

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Sheaf

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasCoproducts A
inst✝³ : HasWeakSheafify J A
inst✝² : HasSeparator A
inst✝¹ : Preadditive A
inst✝ : HasCoproducts A
⊢ (ObjectProperty.ofObj fun x ↦ separator A).IsSeparating

Tactic:
by

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 e ≫ (data X).f j)

Tactic:
by

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
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ 𝟙 { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he }.Y ≫
      { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he }.f =
    (F.map d ≫ F.map b ≫ (data a.Y).f i) ≫ a.f

Tactic:
by

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).toOneHypercover.multicospanShape.L
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.functorPullback F (Sieve.pullback ((data a.Y).f i ≫ a.f) (data X).toPreOneHypercover.sieve₀), ⋯⟩),
    ((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op =
      (s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op

Tactic:
by

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)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
⊢ f₁ ≫ ((data X).toOneHypercover.multifork G).ι i = f₂ ≫ ((data X).toOneHypercover.multifork G).ι i

Tactic:
by

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
⊢ Presheaf.IsSheaf J G ↔
    Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf

Goal state before:
pp: C : Type u
A : Type u₁
K✝ : Type u₂
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} K✝
J : GrothendieckTopology C
inst✝¹ : HasSheafify J A
inst✝ : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A
K : Type u₂
⊢ ∀ [inst : Category.{v₂, u₂} K] [IsFiltered K], HasColimitsOfShape K (Sheaf J A)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf

Goal state before:
pp: C : Type u
A : Type u₁
K✝ : Type u₂
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} K✝
J : GrothendieckTopology C
inst✝³ : HasFiniteLimits A
inst✝² : HasSheafify J A
inst✝¹ : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A
inst✝ : AB5OfSize.{v₂, u₂, v₁, u₁} A
K : Type u₂
x✝¹ : Category.{v₂, u₂} K
x✝ : IsFiltered K
⊢ HasExactColimitsOfShape K (Sheaf J A)

Tactic:
by

Goal state after:
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
T : C
hT : IsTerminal T
F : Cᵒᵖ ⥤ D
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).obj F).map x✝ ≫
      match x✝¹ with
      | Opposite.op X => F.map (hT.from X).op) =
    (match x✝² with
      | Opposite.op X => F.map (hT.from X).op) ≫
      ((𝟭 (Cᵒᵖ ⥤ D)).obj F).map x✝

Tactic:
by

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

Tactic:
by

Goal state after:
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
T : C
hT : IsTerminal T
⊢ ∀ ⦃X Y : Cᵒᵖ ⥤ D⦄ (f : X ⟶ Y),
    ((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).map f ≫
        {
          app := fun x ↦
            match x with
            | Opposite.op X => Y.map (hT.from X).op,
          naturality := ⋯ } =
      {
          app := fun x ↦
            match x with
            | Opposite.op X_1 => X.map (hT.from X_1).op,
          naturality := ⋯ } ≫
        (𝟭 (Cᵒᵖ ⥤ D)).map f

Tactic:
by

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

Tactic:
by

Goal state after:
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 ↔ L.essImage F

Tactic:
by

Goal state after:
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
⊢ IsIso ((constantSheafAdj J D hT).counit.app F)

Tactic:
by

Goal state after:
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
C' : Type u_3
inst✝³ : Category.{v_3, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant J ((sheafEquiv J K G D).inverse.obj F) ↔ IsConstant K F

Tactic:
by

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

Tactic:
by

Goal state after:
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
⊢ ((constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T))).hom ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).hom =
    whiskerRight ((constantSheafAdj J D hT).counit.app F).hom U

Tactic:
constantCommuteCompose_hom_app_hom,

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
⊢ ((sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)))).inv ≫
        sheafifyMap J (constComp Cᵒᵖ (F.obj.obj (Opposite.op T)) U).hom) ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).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
T : C
hT : IsTerminal T
⊢ (constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T)) ≫
      (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F) =
    (sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)

Tactic:
by

Goal state after:
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 ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
h : IsConstant J F
⊢ IsConstant J ((sheafCompose J U).obj F)

Tactic:
by

Goal state after:
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
h : IsConstant J F
⊢ IsConstant J ((sheafCompose J U).obj F)

Tactic:
by
  obtain ⟨Y, ⟨i⟩⟩ := h
  exact ⟨U.obj Y, ⟨(fullyFaithfulSheafToPresheaf _ _).preimageIso
    (((sheafifyComposeIso J U ((const Cᵒᵖ).obj Y)).symm ≪≫
      (presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ Y U)).symm ≪≫
        (sheafToPresheaf _ _).mapIso ((sheafCompose J U).mapIso i))⟩⟩

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
⊢ E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
X : C
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ K.coverings X ↔ E.shrink.presieve₀ ∈ K.coverings X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
⊢ (fun P ↦ P.precoverage) ((fun K ↦ K.preZeroHypercoverFamily) K) = K

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
⊢ (fun K ↦ K.preZeroHypercoverFamily) ((fun P ↦ P.precoverage) P) = P

Tactic:
by

Goal state after:
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
⊢ Presieve.singleton f ∈ P.precoverage.coverings T

Tactic:
by

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
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 b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀

Tactic:
by

Goal state after: