awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h₁ : E.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
R : Presieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
H' :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
rw : Presieve.IsSheafFor F (Sieve.generate R).arrows
⊢ Presieve.IsSheafFor F R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h₁ : E.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
R : Presieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
H' :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
h₁.isSheafFor_sieve_of_pullback h₂ H H'

Premises used: CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h₁ : E.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
R : Presieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
H' :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
exact h₁.isSheafFor_sieve_of_pullback h₂ H H'

Premises used: CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hf : Presieve.IsSeparated J F
rw : Presieve.IsSeparatedFor F (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
⊢ Presieve.IsSeparatedFor F (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)

Tactic:
rw [Presieve.isSeparatedFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSeparatedFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hf : Presieve.IsSeparated J F
⊢ Presieve.IsSeparatedFor F (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows

Tactic:
hf _ E.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hf : Presieve.IsSeparated J F
⊢ Presieve.IsSeparatedFor F (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows

Tactic:
exact hf _ E.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hf : Presieve.IsSheaf J F
rw : Presieve.IsSheafFor F (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
⊢ Presieve.IsSheafFor F (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hf : Presieve.IsSheaf J F
⊢ Presieve.IsSheafFor F (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows

Tactic:
hf _ E.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hf : Presieve.IsSheaf J F
⊢ Presieve.IsSheafFor F (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows

Tactic:
exact hf _ E.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hF : Presieve.IsSheaf J F
S : Sieve.{v_1, u_1} X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
(E.isStronglySheafFor hF).isSheafFor_sieve_of_pullback ?_ h₁ h₂

Premises used: CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback, CategoryTheory.GrothendieckTopology.OneHypercover.isStronglySheafFor
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hF : Presieve.IsSheaf J F
S : Sieve.{v_1, u_1} X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
refine :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
refine (E.isStronglySheafFor hF).isSheafFor_sieve_of_pullback ?_ h₁ h₂

Premises used: CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback, CategoryTheory.GrothendieckTopology.OneHypercover.isStronglySheafFor
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hF : Presieve.IsSheaf J F
S : Sieve.{v_1, u_1} X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
Y : C
f : Y ⟶ X
⊢ Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows

Tactic:
(hF _ (J.pullback_stable _ E.mem₀)).isSeparatedFor

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hF : Presieve.IsSheaf J F
S : Sieve.{v_1, u_1} X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
Y : C
f : Y ⟶ X
⊢ Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows

Tactic:
exact (hF _ (J.pullback_stable _ E.mem₀)).isSeparatedFor

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hF : Presieve.IsSheaf J F
R : Presieve.{v_1, u_1} X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
rw : Presieve.IsSheafFor F (Sieve.generate R).arrows
⊢ Presieve.IsSheafFor F R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hF : Presieve.IsSheaf J F
R : Presieve.{v_1, u_1} X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
E.isSheafFor_sieve_of_pullback hF h₁ h₂

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_sieve_of_pullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
X : C
E : OneHypercover.{w, v_1, u_1} J X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
hF : Presieve.IsSheaf J F
R : Presieve.{v_1, u_1} X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
exact E.isSheafFor_sieve_of_pullback hF h₁ h₂

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_sieve_of_pullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
S T : C
E : OneHypercover.{u_1, v, u} J S
f : (i : E.I₀) → E.X i ⟶ T
h : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), E.p₁ k ≫ f i = E.p₂ k ≫ f j
i : E.I₀
⊢ E.f i ≫ E.glueMorphisms f h = f i

Tactic:
(E.isStronglySheafFor
    (Subcanonical.isSheaf_of_isRepresentable (CategoryTheory.yoneda.obj T))).map_amalgamate _ _ i

Premises used: Quiver.Hom.unop, CategoryTheory.yoneda, CategoryTheory.PreOneHypercover.IsStronglySheafFor.map_amalgamate, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.GrothendieckTopology.OneHypercover.glueMorphisms, CategoryTheory.GrothendieckTopology.OneHypercover.isStronglySheafFor, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
X Y : C
𝒰 : ZeroHypercover.{u_1, v, u} J X
f g : X ⟶ Y
h : ∀ (i : 𝒰.I₀), 𝒰.f i ≫ f = 𝒰.f i ≫ g
⊢ Presieve.IsSheafFor (Functor.obj yoneda Y) (PreZeroHypercover.presieve₀.{u_1, v, u} 𝒰.toPreZeroHypercover)

Tactic:
have hs : 𝒰.presieve₀.IsSheafFor (yoneda.obj Y) :=
    (GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _).isSheafFor_of_mem_precoverage
      𝒰.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
X Y : C
𝒰 : ZeroHypercover.{u_1, v, u} J X
f g : X ⟶ Y
h : ∀ (i : 𝒰.I₀), 𝒰.f i ≫ f = 𝒰.f i ≫ g
hs : Presieve.IsSheafFor (Functor.obj yoneda Y) (PreZeroHypercover.presieve₀.{u_1, v, u} 𝒰.toPreZeroHypercover)
i : 𝒰.I₀
⊢ Eq (α := (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj yoneda Y) (Opposite.op (𝒰.X i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda Y) (𝒰.f i).op) :
          (a : (fun (X : Type v) ↦ X) ((yoneda.obj Y).obj (Opposite.op X))) →
            (fun (X : Type v) ↦ X) ((yoneda.obj Y).obj (Opposite.op (𝒰.X i))))
        f :
      (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj yoneda Y) (Opposite.op (𝒰.X i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda Y) (𝒰.f i).op) :
          (a : (fun (X : Type v) ↦ X) ((yoneda.obj Y).obj (Opposite.op X))) →
            (fun (X : Type v) ↦ X) ((yoneda.obj Y).obj (Opposite.op (𝒰.X i))))
        g :
      (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj yoneda Y) (Opposite.op (𝒰.X i))))

Tactic:
simp [h i]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
X Y : C
𝒰 : ZeroHypercover.{u_1, v, u} J X
f g : X ⟶ Y
h : ∀ (i : 𝒰.I₀), 𝒰.f i ≫ f = 𝒰.f i ≫ g
hs : Presieve.IsSheafFor (Functor.obj yoneda Y) (PreZeroHypercover.presieve₀.{u_1, v, u} 𝒰.toPreZeroHypercover)
⊢ f = g

Tactic:
exact 𝒰.ext_of_isSeparatedFor hs.isSeparatedFor fun i ↦ by simp [h i]

Premises used: CategoryTheory.PreZeroHypercover.ext_of_isSeparatedFor, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
S T : C
𝒰 : ZeroHypercover.{u_1, v, u} J S
inst_2 : 𝒰.HasPullbacks
f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T
hf :
  ∀ (i j : 𝒰.I₀),
    Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ T) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ f i) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ f j)
i : 𝒰.I₀
⊢ 𝒰.f i ≫ 𝒰.glueMorphisms f hf = f i

Tactic:
𝒰.toOneHypercover.f_glueMorphisms _ _ _

Premises used: CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover, CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms, CategoryTheory.Precoverage.ZeroHypercover.glueMorphisms
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
⊢ IsLocalAtTarget (isomorphisms C) J

Tactic:
.mk_of_isStableUnderBaseChange fun {X Y} f 𝒰 (H : ∀ i, IsIso _) ↦ ⟨?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.IsIso.mk, CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
refine_1 :
  {X Y : C} →
    (f : X ⟶ Y) →
      (𝒰 : J.ZeroHypercover Y) → (H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))) → Y ⟶ X
refine_2 :
  ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : J.ZeroHypercover Y)
    (H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))),
    f ≫
        𝒰.glueMorphisms
          (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
          ⋯ =
      𝟙 X
refine_3 :
  ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : J.ZeroHypercover Y)
    (H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))),
    𝒰.glueMorphisms
          (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
          ⋯ ≫
        f =
      𝟙 Y
⊢ IsLocalAtTarget (isomorphisms C) J

Tactic:
refine .mk_of_isStableUnderBaseChange fun {X Y} f 𝒰 (H : ∀ i, IsIso _) ↦ ⟨?_, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
refine_1 :
  ∀ (i j : 𝒰.I₀),
    Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ X)
      (pullback.fst (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
          i)
      (pullback.snd (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
          j)
⊢ Y ⟶ X

Tactic:
refine 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst _ _) fun i j ↦ ?_

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, CategoryTheory.Precoverage.ZeroHypercover.glueMorphisms, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ Eq (α := pullback f (𝒰.f i) ⟶ Y) ((pullback.fst f (𝒰.f i) ≫ f) ≫ 𝟙 Y) (pullback.snd f (𝒰.f i) ≫ 𝒰.f i)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 Y = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f_1 : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f_1 (𝒰.f i)) (pullback.snd f_1 (𝒰.f i))
i j : 𝒰.I₀
f : pullback (X := pullback f_1 (𝒰.f i)) (pullback.fst f_1 (𝒰.f i) ≫ f_1) (𝒰.f j) ⟶ pullback (𝒰.f i) (𝒰.f j) :=
  pullback.map (pullback.fst f_1 (𝒰.f i) ≫ f_1) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd f_1 (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯
refine_1 :
  Eq (α :=
    pullback (X := pullback f_1 (𝒰.f i)) (Y := pullback f_1 (𝒰.f j)) (pullback.fst f_1 (𝒰.f i))
        (pullback.fst f_1 (𝒰.f j)) ⟶
      X)
    ((Iso.hom (pullbackRightPullbackFstIso f_1 (𝒰.f j) (pullback.fst f_1 (𝒰.f i))) ≫ f) ≫
      pullback.fst (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
          i)
    ((Iso.hom (pullbackRightPullbackFstIso f_1 (𝒰.f j) (pullback.fst f_1 (𝒰.f i))) ≫ f) ≫
      pullback.snd (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
          j)
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ X)
    (pullback.fst (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
        i)
    (pullback.snd (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
        j)

Tactic:
rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ f)]

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f_1 : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f_1 (𝒰.f i)) (pullback.snd f_1 (𝒰.f i))
i j : 𝒰.I₀
f : pullback (X := pullback f_1 (𝒰.f i)) (pullback.fst f_1 (𝒰.f i) ≫ f_1) (𝒰.f j) ⟶ pullback (𝒰.f i) (𝒰.f j) :=
  pullback.map (pullback.fst f_1 (𝒰.f i) ≫ f_1) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd f_1 (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯
⊢ Eq (α :=
    pullback (X := pullback f_1 (𝒰.f i)) (Y := pullback f_1 (𝒰.f j)) (pullback.fst f_1 (𝒰.f i))
        (pullback.fst f_1 (𝒰.f j)) ⟶
      X)
    ((Iso.hom (pullbackRightPullbackFstIso f_1 (𝒰.f j) (pullback.fst f_1 (𝒰.f i))) ≫ f) ≫
      pullback.fst (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
          i)
    ((Iso.hom (pullbackRightPullbackFstIso f_1 (𝒰.f j) (pullback.fst f_1 (𝒰.f i))) ≫ f) ≫
      pullback.snd (𝒰.f i) (𝒰.f j) ≫
        (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
          j)

Tactic:
simp [pullback.condition, f]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : (pullback₁ f 𝒰).I₀
⊢ (pullback₁ f 𝒰).f i ≫
      f ≫
        𝒰.glueMorphisms
          (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
          ⋯ =
    (pullback₁ f 𝒰).f i ≫ 𝟙 X

Tactic:
simp [pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ f ≫
      𝒰.glueMorphisms
        (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
        ⋯ =
    𝟙 X

Tactic:
exact (𝒰.pullback₁ f).hom_ext fun i ↦ by simp [pullback.condition_assoc]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.hom_ext, CategoryTheory.Precoverage.ZeroHypercover.pullback₁