awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.IsCocontinuous J K
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
hS :
  Membership.mem (α := Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left) (γ :=
    Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
    ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
          (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S :
      Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)
⊢ Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    (Sieve.functorPullback F
      ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
          (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))

Tactic:
exact F.cover_lift J K hS

Premises used: CategoryTheory.Functor.cover_lift
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
h : CoverPreserving J K F
U : Over.{v, u} X
S : Sieve U
hS : S ∈ (J.over X : (a : Over X) → Set (Sieve a)) U
rw :
  ∀
    (hS :
      Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
        ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) S : Sieve.{v, u} U.left)),
    Membership.mem (α := Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left) (γ :=
      Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
      ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
      ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
            (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
          (Sieve.functorPushforward (Over.post F) S) :
        Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)
⊢ Membership.mem (γ := Set (Sieve (Functor.obj (Over.post F) U)))
    ((K.over (F.obj X) : (a : Over (F.obj X)) → Set (Sieve a)) (Functor.obj (Over.post F) U))
    (Sieve.functorPushforward (Over.post F) S)

Tactic:
rw [GrothendieckTopology.mem_over_iff] at hS ⊢

Premises used: CategoryTheory.GrothendieckTopology.mem_over_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
h : CoverPreserving J K F
U : Over.{v, u} X
S : Sieve U
hS :
  Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) S : Sieve.{v, u} U.left)
rw :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
    (Sieve.functorPushforward F ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) S))
⊢ Membership.mem (α := Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left) (γ :=
    Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
    ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
          (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        (Sieve.functorPushforward (Over.post F) S) :
      Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)

Tactic:
rw [Sieve.overEquiv_functorPushforward_post]

Premises used: CategoryTheory.Sieve.overEquiv_functorPushforward_post
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
h : CoverPreserving J K F
U : Over.{v, u} X
S : Sieve U
hS :
  Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) S : Sieve.{v, u} U.left)
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
    (Sieve.functorPushforward F ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) S))

Tactic:
h.cover_preserve hS

Premises used: Set.Mem, CategoryTheory.CoverPreserving.cover_preserve
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
h : CoverPreserving J K F
U : Over.{v, u} X
S : Sieve U
hS :
  Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) S : Sieve.{v, u} U.left)
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
    (Sieve.functorPushforward F ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) S))

Tactic:
exact h.cover_preserve hS

Premises used: CategoryTheory.CoverPreserving.cover_preserve
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
⊢ E.IsPreservedBy (Over.forget X) J

Tactic:
⟨?_, ?_⟩

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mk
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
refine_1 :
  Membership.mem (γ := Set (Sieve.{v, u} (Functor.obj (Over.forget X) Y)))
    ((J : (a : C) → Set (Sieve a)) (Functor.obj (Over.forget X) Y))
    (PreZeroHypercover.sieve₀.{u_1, v, u} (E.map (Over.forget X)).toPreZeroHypercover)
refine_2 :
  ∀ (i₁ i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ Functor.obj (Over.forget X) (E.X i₁))
    (p₂ : W ⟶ Functor.obj (Over.forget X) (E.X i₂))
    (w : p₁ ≫ Functor.map (Over.forget X) (E.f i₁) = p₂ ≫ Functor.map (Over.forget X) (E.f i₂)),
    (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ (J : (a : C) → Set (Sieve a)) W
⊢ E.IsPreservedBy (Over.forget X) J

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
refine_1 :
  Membership.mem (γ := Set (Sieve.{v, u} Y.left)) ((J : (a : C) → Set (Sieve a)) Y.left)
    (PreZeroHypercover.sieve₀.{u_1, v, u} (PreZeroHypercover.map (Over.forget X) E.toPreZeroHypercover))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (Functor.obj (Over.forget X) Y)))
    ((J : (a : C) → Set (Sieve a)) (Functor.obj (Over.forget X) Y))
    (PreZeroHypercover.sieve₀.{u_1, v, u} (E.map (Over.forget X)).toPreZeroHypercover)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
refine_1 :
  Membership.mem (γ := Set (Sieve.{v, u} Y.left)) ((J : (a : C) → Set (Sieve a)) Y.left)
    (Sieve.functorPushforward (Over.forget X) E.sieve₀)
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y.left)) ((J : (a : C) → Set (Sieve a)) Y.left)
    (PreZeroHypercover.sieve₀.{u_1, v, u} (PreZeroHypercover.map (Over.forget X) E.toPreZeroHypercover))

Tactic:
rw [dsimp% PreZeroHypercover.sieve₀_map (F := Over.forget X)]

Premises used: CategoryTheory.PreZeroHypercover.sieve₀_map
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y.left)) ((J : (a : C) → Set (Sieve a)) Y.left)
    (Sieve.functorPushforward (Over.forget X) E.sieve₀)

Tactic:
E.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, Set.Mem, setOf, Set.preimage, CategoryTheory.Sieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y.left)) ((J : (a : C) → Set (Sieve a)) Y.left)
    (Sieve.functorPushforward (Over.forget X) E.sieve₀)

Tactic:
exact E.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ Functor.obj (Over.forget X) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.forget X) (E.X i₂)
w : p₁ ≫ Functor.map (Over.forget X) (E.f i₁) = p₂ ≫ Functor.map (Over.forget X) (E.f i₂)
⊢ (p₁ ≫ Functor.map (Over.forget X) (E.f i₁)) ≫ Y.hom = (p₂ ≫ Functor.map (Over.forget X) (E.f i₂)) ≫ Y.hom

Tactic:
have := w =≫ Over.hom _
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ Functor.obj (Over.forget X) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.forget X) (E.X i₂)
w : p₁ ≫ Functor.map (Over.forget X) (E.f i₁) = p₂ ≫ Functor.map (Over.forget X) (E.f i₂)
this : (p₁ ≫ Functor.map (Over.forget X) (E.f i₁)) ≫ Y.hom = (p₂ ≫ Functor.map (Over.forget X) (E.f i₂)) ≫ Y.hom
⊢ p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom

Tactic:
simp only [Over.forget_obj, Over.forget_map, Category.assoc, Over.w] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.forget_obj, CategoryTheory.Over.w, CategoryTheory.Over.forget_map
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ Functor.obj (Over.forget X) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.forget X) (E.X i₂)
w : p₁ ≫ Functor.map (Over.forget X) (E.f i₁) = p₂ ≫ Functor.map (Over.forget X) (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
h :
  Eq (α := (Over.mk (p₁ ≫ (E.X i₁).hom)).left ⟶ Y.left) (Over.Hom.left (Over.homMk p₁ ⋯ ≫ E.f i₁))
    (Over.Hom.left (Over.homMk p₂ ⋯ ≫ E.f i₂))
⊢ Eq (α := Over.mk (p₁ ≫ (E.X i₁).hom) ⟶ Y) (Over.homMk p₁ ⋯ ≫ E.f i₁) (Over.homMk p₂ ⋯ ≫ E.f i₂)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ Functor.obj (Over.forget X) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.forget X) (E.X i₂)
w : p₁ ≫ Functor.map (Over.forget X) (E.f i₁) = p₂ ≫ Functor.map (Over.forget X) (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
⊢ Eq (α := (Over.mk (p₁ ≫ (E.X i₁).hom)).left ⟶ Y.left) (Over.Hom.left (Over.homMk p₁ ⋯ ≫ E.f i₁))
    (Over.Hom.left (Over.homMk p₂ ⋯ ≫ E.f i₂))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ Functor.obj (Over.forget X) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.forget X) (E.X i₂)
w : p₁ ≫ Functor.map (Over.forget X) (E.f i₁) = p₂ ≫ Functor.map (Over.forget X) (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
⊢ Membership.mem (γ := Set (Sieve (Over.mk (p₁ ≫ (E.X i₁).hom))))
    ((J.over X : (a : Over X) → Set (Sieve a)) (Over.mk (p₁ ≫ (E.X i₁).hom)))
    (E.sieve₁ (i₁ := i₁) (i₂ := i₂) (Over.homMk p₁ ⋯) (Over.homMk p₂ ⋯))

Tactic:
have := E.mem₁ i₁ i₂ (Over.homMk (U := Over.mk (p₁ ≫ Over.hom _)) p₁)
      (Over.homMk (U := Over.mk (p₁ ≫ Over.hom _)) p₂ this.symm) (by ext; simpa)
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ Functor.obj (Over.forget X) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.forget X) (E.X i₂)
w : p₁ ≫ Functor.map (Over.forget X) (E.f i₁) = p₂ ≫ Functor.map (Over.forget X) (E.f i₂)
this_1 : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
this :
  Membership.mem (γ := Set (Sieve (Over.mk (p₁ ≫ (E.X i₁).hom))))
    ((J.over X : (a : Over X) → Set (Sieve a)) (Over.mk (p₁ ≫ (E.X i₁).hom)))
    (E.sieve₁ (i₁ := i₁) (i₂ := i₂) (Over.homMk p₁ ⋯) (Over.homMk p₂ ⋯))
refine_2 :
  ∀
    (this :
      Membership.mem (α := Sieve.{v, u} (Over.mk (p₁ ≫ (E.X i₁).hom)).left) (γ :=
        Set (Sieve.{v, u} (Over.mk (p₁ ≫ (E.X i₁).hom)).left))
        ((J : (a : C) → Set (Sieve a)) (Over.mk (p₁ ≫ (E.X i₁).hom)).left)
        ((Sieve.overEquiv (Over.mk (p₁ ≫ (E.X i₁).hom)) :
              (a : Sieve (Over.mk (p₁ ≫ (E.X i₁).hom))) → Sieve (Over.mk (p₁ ≫ (E.X i₁).hom)).left)
            (E.sieve₁ (i₁ := i₁) (i₂ := i₂) (Over.homMk p₁ ⋯) (Over.homMk p₂ ⋯)) :
          Sieve.{v, u} (Over.mk (p₁ ≫ (E.X i₁).hom)).left)),
    (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ (J : (a : C) → Set (Sieve a)) W
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀
    (this :
      Membership.mem (γ := Set (Sieve.{v, u} (Over.mk (p₁ ≫ (E.X i₁).hom)).left))
        ((J : (a : C) → Set (Sieve a)) (Over.mk (p₁ ≫ (E.X i₁).hom)).left)
        ((E.map (Over.forget X)).sieve₁ (i₁ := i₁) (i₂ := i₂) (Over.Hom.left (Over.homMk p₁ ⋯))
          (Over.Hom.left (Over.homMk p₂ ⋯)))),
    (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ (J : (a : C) → Set (Sieve a)) W
⊢ (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ (J : (a : C) → Set (Sieve a)) W

Tactic:
rwa [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_preOneHypercover_sieve₁] at this

Premises used: CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.Sieve.overEquiv_preOneHypercover_sieve₁
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
⊢ E.IsPreservedBy (Over.post F) (K.over (F.obj X))

Tactic:
⟨?_, ?_⟩

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mk
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
refine_1 :
  Membership.mem (γ := Set (Sieve (Functor.obj (Over.post F) Y)))
    ((K.over (F.obj X) : (a : Over (F.obj X)) → Set (Sieve a)) (Functor.obj (Over.post F) Y))
    (E.map (Over.post F)).sieve₀
refine_2 :
  ∀ (i₁ i₂ : E.I₀) ⦃W : Over.{v_1, u_1} (F.obj X)⦄ (p₁ : W ⟶ Functor.obj (Over.post F) (E.X i₁))
    (p₂ : W ⟶ Functor.obj (Over.post F) (E.X i₂))
    (w : p₁ ≫ Functor.map (Over.post F) (E.f i₁) = p₂ ≫ Functor.map (Over.post F) (E.f i₂)),
    (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X) : (a : Over (F.obj X)) → Set (Sieve a)) W
⊢ E.IsPreservedBy (Over.post F) (K.over (F.obj X))

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
refine_1 :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) Y).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) Y).left)
    (Sieve.ofArrows (fun (i : E.I₀) ↦ (Functor.obj (Over.post F) (E.X i)).left) fun (i : E.I₀) ↦
      Over.Hom.left (Functor.map (Over.post F) (E.f i)))
⊢ Membership.mem (γ := Set (Sieve (Functor.obj (Over.post F) Y)))
    ((K.over (F.obj X) : (a : Over (F.obj X)) → Set (Sieve a)) (Functor.obj (Over.post F) Y))
    (PreZeroHypercover.sieve₀ (PreZeroHypercover.map (Over.post F) E.toPreZeroHypercover))

Tactic:
rw [PreZeroHypercover.sieve₀_map, GrothendieckTopology.mem_over_iff,
      Sieve.functorPushforward_ofArrows, Sieve.overEquiv_ofArrows]

Premises used: CategoryTheory.Sieve.overEquiv_ofArrows, CategoryTheory.PreZeroHypercover.sieve₀_map, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.Sieve.functorPushforward_ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) Y).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) Y).left)
    (Sieve.ofArrows (fun (i : E.I₀) ↦ (Functor.obj (Over.post F) (E.X i)).left) fun (i : E.I₀) ↦
      Over.Hom.left (Functor.map (Over.post F) (E.f i)))

Tactic:
E'.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, Set.Mem
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) Y).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) Y).left)
    (Sieve.ofArrows (fun (i : E.I₀) ↦ (Functor.obj (Over.post F) (E.X i)).left) fun (i : E.I₀) ↦
      Over.Hom.left (Functor.map (Over.post F) (E.f i)))

Tactic:
exact E'.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over.{v_1, u_1} (F.obj X)
p₁ : W ⟶ Functor.obj (Over.post F) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.post F) (E.X i₂)
w : p₁ ≫ Functor.map (Over.post F) (E.f i₁) = p₂ ≫ Functor.map (Over.post F) (E.f i₂)
refine_2 :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} W.left)) ((K : (a : D) → Set (Sieve a)) W.left)
    (((E.map (Over.forget X)).map F).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂))
⊢ (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X) : (a : Over (F.obj X)) → Set (Sieve a)) W

Tactic:
simp_rw [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_preOneHypercover_sieve₁,
      ← PreOneHypercover.map_comp, Over.post_forget_eq_forget_comp, PreOneHypercover.map_comp]

Premises used: CategoryTheory.PreOneHypercover.map_comp, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.Sieve.overEquiv_preOneHypercover_sieve₁, CategoryTheory.Over.post_forget_eq_forget_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over.{v_1, u_1} (F.obj X)
p₁ : W ⟶ Functor.obj (Over.post F) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.post F) (E.X i₂)
w : p₁ ≫ Functor.map (Over.post F) (E.f i₁) = p₂ ≫ Functor.map (Over.post F) (E.f i₂)
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} W.left)) ((K : (a : D) → Set (Sieve a)) W.left)
    (((E.map (Over.forget X)).map F).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂))

Tactic:
E'.mem₁ _ _ _ _ congr($(w).left)

Premises used: congrArg, Set.Mem, CategoryTheory.Over.Hom.left, CategoryTheory.PreOneHypercover.map, id, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.PreservesOneHypercovers J K
Y : Over.{v, u} X
E : (J.over X).OneHypercover Y
E' : OneHypercover.{w, v_1, u_1} K (F.obj (Functor.obj (Over.forget X) Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over.{v_1, u_1} (F.obj X)
p₁ : W ⟶ Functor.obj (Over.post F) (E.X i₁)
p₂ : W ⟶ Functor.obj (Over.post F) (E.X i₂)
w : p₁ ≫ Functor.map (Over.post F) (E.f i₁) = p₂ ≫ Functor.map (Over.post F) (E.f i₂)
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} W.left)) ((K : (a : D) → Set (Sieve a)) W.left)
    (((E.map (Over.forget X)).map F).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂))

Tactic:
exact E'.mem₁ _ _ _ _ congr($(w).left)

Premises used: congrArg, CategoryTheory.Over.Hom.left, id, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : X ⟶ Y
rw : (Over.map f).IsCocontinuous (J.over X) (J.over Y)
⊢ CoverPreserving (J.over Y) (J.over X) (Over.pullback f)

Tactic:
rw [← (Over.mapPullbackAdj f).isCocontinuous_iff_coverPreserving]

Premises used: CategoryTheory.Adjunction.isCocontinuous_iff_coverPreserving, CategoryTheory.Over.mapPullbackAdj
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (Over.map f).IsCocontinuous (J.over X) (J.over Y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (Over.pullback f).IsContinuous (J.over Y) (J.over X)

Tactic:
(Over.mapPullbackAdj f).isContinuous_of_isCocontinuous _ _

Premises used: CategoryTheory.Over.mapPullbackAdj, CategoryTheory.Adjunction.isContinuous_of_isCocontinuous
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u'
inst : Category.{v_1, u'} C
inst_1 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X U : C
S : Sieve.{v_1, u'} U
hs : S ∈ (J : (a : C) → Set (Sieve a)) U
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v_1, u'} X) (Functor.obj (Over.star X) U)))
    ((J.over X : (a : Over X) → Set (Sieve a)) (Functor.obj (Over.star X) U)) (Sieve.functorPushforward (Over.star X) S)

Tactic:
J.superset_covering ?_ (J.pullback_stable prod.snd hs)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, Set.Mem, setOf, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Limits.prod.snd, Set.preimage