awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }
hR :
  Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    ((K.toGrothendieck.over X : (a : Over X) → Set (Sieve a)) { left := Y, right := right, hom := s }) R
refine_1 :
  ∀ (R : Sieve.{v, u} Y)
    (hR :
      Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
        Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
        ((K.toGrothendieck.over X : (a : Over X) → Set (Sieve a)) { left := Y, right := right, hom := s })
        ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
              (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
                Sieve { left := Y, right := right, hom := s })
            R :
          Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
              Sieve { left := Y, right := right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    R

Tactic:
obtain ⟨(R : Sieve Y), rfl⟩ := (Sieve.overEquiv _).symm.surjective R

Premises used: CategoryTheory.Sieve.overEquiv, CategoryTheory.Sieve, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve.{v, u} Y
hR :
  Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    ((K.toGrothendieck.over X : (a : Over X) → Set (Sieve a)) { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        R :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
⊢ K.toCoverage.Saturate Y R

Tactic:
simp +instances only [GrothendieckTopology.mem_over_iff, Equiv.apply_symm_apply,
      ← Precoverage.toGrothendieck_toCoverage, Coverage.mem_toGrothendieck,
      Over.left] at hR

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.Over.left, CategoryTheory.Coverage.mem_toGrothendieck, CategoryTheory.Precoverage.toGrothendieck_toCoverage
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve.{v, u} Y
Z : C
S : Presieve.{v, u} Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
refine_1 :
  Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Z, right := right, hom := s })
    (Sieve.generate (Presieve.functorPullback (Over.forget X) S))
⊢ Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Z, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Z, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Z, right := right, hom := s })) →
            Sieve { left := Z, right := right, hom := s })
        (Sieve.generate S) :
      Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s })

Tactic:
rw [Sieve.overEquiv_symm_generate]

Premises used: CategoryTheory.Sieve.overEquiv_symm_generate
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve.{v, u} Y
Z : C
S : Presieve.{v, u} Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Membership.mem (γ := Set (Presieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
    ((Precoverage.comap (Over.forget X) K).coverings { left := Z, right := right, hom := s })
    (Presieve.functorPullback (Over.forget X) S)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve.{v, u} Y
Z : C
S : Presieve.{v, u} Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Z, right := right, hom := s })
    (Sieve.generate (Presieve.functorPullback (Over.forget X) S))

Tactic:
exact .of _ _ (by simpa)
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve.{v, u} Y
X_1 : C
s : X_1 ⟶ X
refine_1 :
  Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := X_1, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := X_1, right := right, hom := s })
    ⊤
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := X_1, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := X_1, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := X_1, right := right, hom := s }) :
        (a : Sieve (Over.left { left := X_1, right := right, hom := s })) →
          Sieve { left := X_1, right := right, hom := s })
      ⊤)

Tactic:
rw [Sieve.overEquiv_symm_top]

Premises used: CategoryTheory.Sieve.overEquiv_symm_top
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve.{v, u} Y
X_1 : C
s : X_1 ⟶ X
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := X_1, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := X_1, right := right, hom := s })
    ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y_1 : C
right : Discrete PUnit.{1}
R_1 : Sieve.{v, u} Y_1
Y : C
R S : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_2 (Sieve.pullback f S)
ih :
  ∀ (s : Y ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
              Sieve { left := Y, right := right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
ih' :
  ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_2 ⟶ X),
        Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s }) (γ :=
          Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s }))
          (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
            { left := Y_2, right := right, hom := s })
          ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := right, hom := s }) :
                (a : Sieve (Over.left { left := Y_2, right := right, hom := s })) →
                  Sieve { left := Y_2, right := right, hom := s })
              (Sieve.pullback f S) :
            Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s })
s : Y ⟶ X
⊢ Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        S :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })

Tactic:
GrothendieckTopology.transitive _ (ih s) _ fun Z g hg ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y_1 : C
right : Discrete PUnit.{1}
R_1 : Sieve.{v, u} Y_1
Y : C
R S : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_2 (Sieve.pullback f S)
ih :
  ∀ (s : Y ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
              Sieve { left := Y, right := right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
ih' :
  ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_2 ⟶ X),
        Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s }) (γ :=
          Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s }))
          (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
            { left := Y_2, right := right, hom := s })
          ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := right, hom := s }) :
                (a : Sieve (Over.left { left := Y_2, right := right, hom := s })) →
                  Sieve { left := Y_2, right := right, hom := s })
              (Sieve.pullback f S) :
            Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s })
s : Y ⟶ X
Z : Over.{v, u} X
g : Z ⟶ { left := Y, right := right, hom := s }
hg :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
        (a : Sieve (Over.left { left := Y, right := right, hom := s })) → Sieve { left := Y, right := right, hom := s })
      R)
    g
⊢ right = Z.right

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y_1 : C
R_1 : Sieve.{v, u} Y_1
Y : C
R S : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_2 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over.{v, u} X
ih :
  ∀ (s : Y ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := Z.right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
              Sieve { left := Y, right := Z.right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s })
ih' :
  ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_2 ⟶ X),
        Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }) (γ :=
          Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }))
          (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
            { left := Y_2, right := Z.right, hom := s })
          ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := Z.right, hom := s }) :
                (a : Sieve (Over.left { left := Y_2, right := Z.right, hom := s })) →
                  Sieve { left := Y_2, right := Z.right, hom := s })
              (Sieve.pullback f S) :
            Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s })
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
        (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
          Sieve { left := Y, right := Z.right, hom := s })
      R)
    g
refine_1 :
  Membership.mem (α := Sieve Z)
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z)
    (((Sieve.overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) (Sieve.pullback (Over.Hom.left g) S) : Sieve Z)
⊢ Sieve.pullback g
      ((Equiv.symm
            (Sieve.overEquiv
              { left := Y, right := Z.right, hom := s : Comma.{v, 0, v, u, 0, u} (𝟭 C) (Functor.fromPUnit X) }) :
          (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
            Sieve { left := Y, right := Z.right, hom := s })
        S) ∈
    ((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z

Tactic:
rw [← Sieve.overEquiv_symm_pullback]

Premises used: CategoryTheory.Sieve.overEquiv_symm_pullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y_1 : C
R_1 : Sieve.{v, u} Y_1
Y : C
R S : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_2 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over.{v, u} X
ih :
  ∀ (s : Y ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := Z.right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
              Sieve { left := Y, right := Z.right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s })
ih' :
  ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_2 ⟶ X),
        Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }) (γ :=
          Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }))
          (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
            { left := Y_2, right := Z.right, hom := s })
          ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := Z.right, hom := s }) :
                (a : Sieve (Over.left { left := Y_2, right := Z.right, hom := s })) →
                  Sieve { left := Y_2, right := Z.right, hom := s })
              (Sieve.pullback f S) :
            Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s })
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
        (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
          Sieve { left := Y, right := Z.right, hom := s })
      R)
    g
⊢ Membership.mem (α := Sieve Z)
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z)
    (((Sieve.overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) (Sieve.pullback (Over.Hom.left g) S) : Sieve Z)

Tactic:
ih' hg Z.hom

Premises used: CategoryTheory.Over, Set.Mem, setOf, CategoryTheory.CostructuredArrow, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y_1 : C
R_1 : Sieve.{v, u} Y_1
Y : C
R S : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_2 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over.{v, u} X
ih :
  ∀ (s : Y ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := Z.right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
              Sieve { left := Y, right := Z.right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s })
ih' :
  ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_2 ⟶ X),
        Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }) (γ :=
          Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }))
          (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
            { left := Y_2, right := Z.right, hom := s })
          ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := Z.right, hom := s }) :
                (a : Sieve (Over.left { left := Y_2, right := Z.right, hom := s })) →
                  Sieve { left := Y_2, right := Z.right, hom := s })
              (Sieve.pullback f S) :
            Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s })
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
        (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
          Sieve { left := Y, right := Z.right, hom := s })
      R)
    g
⊢ Membership.mem (α := Sieve Z)
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z)
    (((Sieve.overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) (Sieve.pullback (Over.Hom.left g) S) : Sieve Z)

Tactic:
exact ih' hg Z.hom

Premises used: CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
refine_2 : Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage
⊢ (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X

Tactic:
rw [Precoverage.toGrothendieck_le_iff_le_toPrecoverage]

Premises used: CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
Y : Over.{v, u} X
R : Presieve Y
hR : R ∈ (Precoverage.comap (Over.forget X) K).coverings Y
⊢ Membership.mem (γ := Set (Presieve.{v, u} (Functor.obj (Over.forget X) Y)))
    (K.coverings (Functor.obj (Over.forget X) Y)) (Presieve.map (Over.forget X) R)

Tactic:
rw [Precoverage.mem_comap_iff] at hR

Premises used: CategoryTheory.Precoverage.mem_comap_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
Y : Over.{v, u} X
R : Presieve Y
hR :
  Membership.mem (γ := Set (Presieve.{v, u} (Functor.obj (Over.forget X) Y)))
    (K.coverings (Functor.obj (Over.forget X) Y)) (Presieve.map (Over.forget X) R)
refine_2 :
  Membership.mem (α := Sieve.{v, u} Y.left) (γ := Set (Sieve.{v, u} Y.left))
    ((K.toGrothendieck : (a : C) → Set (Sieve a)) Y.left)
    (Sieve.generate (Presieve.map (Over.forget X) R) : Sieve.{v, u} (Functor.obj (Over.forget X) Y))
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y

Tactic:
rw [GrothendieckTopology.mem_toPrecoverage_iff, GrothendieckTopology.mem_over_iff,
      Sieve.overEquiv, Equiv.coe_fn_mk, ← Sieve.generate_map_eq_functorPushforward]

Premises used: CategoryTheory.Sieve.overEquiv, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff, CategoryTheory.Sieve.generate_map_eq_functorPushforward, Equiv.coe_fn_mk
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
Y : Over.{v, u} X
R : Presieve Y
hR :
  Membership.mem (γ := Set (Presieve.{v, u} (Functor.obj (Over.forget X) Y)))
    (K.coverings (Functor.obj (Over.forget X) Y)) (Presieve.map (Over.forget X) R)
⊢ Membership.mem (α := Sieve.{v, u} Y.left) (γ := Set (Sieve.{v, u} Y.left))
    ((K.toGrothendieck : (a : C) → Set (Sieve a)) Y.left)
    (Sieve.generate (Presieve.map (Over.forget X) R) : Sieve.{v, u} (Functor.obj (Over.forget X) Y))

Tactic:
Precoverage.Saturate.of _ _ hR

Premises used: Set.Mem, setOf, CategoryTheory.Precoverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
Y : Over.{v, u} X
R : Presieve Y
hR :
  Membership.mem (γ := Set (Presieve.{v, u} (Functor.obj (Over.forget X) Y)))
    (K.coverings (Functor.obj (Over.forget X) Y)) (Presieve.map (Over.forget X) R)
⊢ Membership.mem (α := Sieve.{v, u} Y.left) (γ := Set (Sieve.{v, u} Y.left))
    ((K.toGrothendieck : (a : C) → Set (Sieve a)) Y.left)
    (Sieve.generate (Presieve.map (Over.forget X) R) : Sieve.{v, u} (Functor.obj (Over.forget X) Y))

Tactic:
exact Precoverage.Saturate.of _ _ hR

Premises used: CategoryTheory.Precoverage.Saturate.of