awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (obj (Over.forget X) Y)))
    ((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) (↑T : Sieve ((Over.forget X).obj Y))

Tactic:
T.property

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
h :
  Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))) =
    (↑T : Sieve ((Over.forget X).obj Y))
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (obj (Over.forget X) Y)))
    ((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y))
    (Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))

Tactic:
convert! T.property

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
h :
  ∀ ⦃Z : C⦄ (f : Z ⟶ obj (Over.forget X) Y),
    Sieve.arrows
        (Sieve.functorPushforward (Over.forget X)
          (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
        f ↔
      (↑T : Sieve ((Over.forget X).obj Y)).arrows f
⊢ Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))) =
    (↑T : Sieve ((Over.forget X).obj Y))

Tactic:
ext Z f
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
Z : C
f : Z ⟶ obj (Over.forget X) Y
h :
  Sieve.arrows
      (Sieve.functorPushforward (Over.forget X)
        (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
      f →
    (↑T : Sieve ((Over.forget X).obj Y)).arrows f
h₁ :
  (↑T : Sieve ((Over.forget X).obj Y)).arrows f →
    Sieve.arrows
      (Sieve.functorPushforward (Over.forget X)
        (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
      f
⊢ Sieve.arrows
      (Sieve.functorPushforward (Over.forget X)
        (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
      f ↔
    (↑T : Sieve ((Over.forget X).obj Y)).arrows f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
Z : C
w : Over.{v_1, u_1} X
w_1 : w ⟶ Y
g' : Z ⟶ obj (Over.forget X) w
hg : (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))).arrows w_1
⊢ (↑T : Sieve ((Over.forget X).obj Y)).arrows (g' ≫ map (Over.forget X) w_1)

Tactic:
T.val.downward_closed hg g'

Premises used: CategoryTheory.Sieve.downward_closed, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
Z : C
w : Over.{v_1, u_1} X
w_1 : w ⟶ Y
g' : Z ⟶ obj (Over.forget X) w
hg : (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))).arrows w_1
⊢ (↑T : Sieve ((Over.forget X).obj Y)).arrows (g' ≫ map (Over.forget X) w_1)

Tactic:
exact T.val.downward_closed hg g'

Premises used: CategoryTheory.Sieve.downward_closed, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
Z : C
f : Z ⟶ obj (Over.forget X) Y
hf : (↑T : Sieve ((Over.forget X).obj Y)).arrows f
⊢ Sieve.arrows
    (Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
    f

Tactic:
⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩

Premises used: CategoryTheory.Over.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.Over.homMk, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, Eq.symm, CategoryTheory.Over.hom, CategoryTheory.Presieve.functorPushforward, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
Z : C
f : Z ⟶ obj (Over.forget X) Y
hf : (↑T : Sieve ((Over.forget X).obj Y)).arrows f
⊢ Sieve.arrows
    (Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
    f

Tactic:
exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
rw : comap F K ≤ (F.inducedTopology K.toGrothendieck).toPrecoverage
⊢ (comap F K).toGrothendieck ≤ F.inducedTopology K.toGrothendieck

Tactic:
rw [Precoverage.toGrothendieck_le_iff_le_toPrecoverage]

Premises used: CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
X : C
R : Presieve.{v_3, u_3} X
hR : R ∈ (comap F K).coverings X
⊢ Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) (map F R)

Tactic:
rw [Precoverage.mem_comap_iff] at hR

Premises used: CategoryTheory.Precoverage.mem_comap_iff
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
X : C
R : Presieve.{v_3, u_3} X
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) (map F R)
rw :
  Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj X))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj X))
    (Sieve.generate (map F R))
⊢ R ∈ (F.inducedTopology K.toGrothendieck).toPrecoverage.coverings X

Tactic:
rw [GrothendieckTopology.mem_toPrecoverage_iff, Functor.mem_inducedTopology_sieves_iff,
    ← Sieve.generate_map_eq_functorPushforward]

Premises used: CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff, CategoryTheory.Sieve.generate_map_eq_functorPushforward, CategoryTheory.Functor.mem_inducedTopology_sieves_iff
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
X : C
R : Presieve.{v_3, u_3} X
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) (map F R)
⊢ Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj X))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj X))
    (Sieve.generate (map F R))

Tactic:
Precoverage.generate_mem_toGrothendieck hR

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
X : C
R : Presieve.{v_3, u_3} X
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) (map F R)
⊢ Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj X))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj X))
    (Sieve.generate (map F R))

Tactic:
exact Precoverage.generate_mem_toGrothendieck hR

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
rw :
  ∀
    (hT_1 :
      ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
        Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧ R ≤ T.arrows),
    ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
        R ≤
          (Sieve.functorPushforward F
              (Sieve.functorPullback F
                (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                      Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                        ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                      T hT) :
                  Sieve (F.obj U)))).arrows
⊢ Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U))
    (Sieve.functorPushforward F
      (Sieve.functorPullback F
        (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
              Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
              T hT) :
          Sieve (F.obj U))))

Tactic:
rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT ⊢

Premises used: CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT_1 : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
hT :
  ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧ R ≤ T.arrows
obtain :
  ∀ (R : Presieve.{v_4, u_4} (F.obj U))
    (hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R) (hle : R ≤ T.arrows),
    ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
        R ≤
          (Sieve.functorPushforward F
              (Sieve.functorPullback F
                (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                      Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                        ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                      T hT_1) :
                  Sieve (F.obj U)))).arrows
⊢ ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
      R ≤
        (Sieve.functorPushforward F
            (Sieve.functorPullback F
              (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                    Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                      ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                    T hT_1) :
                Sieve (F.obj U)))).arrows

Tactic:
obtain ⟨R, hR, hle⟩ := hT
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
R : Presieve.{v_4, u_4} (F.obj U)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R
hle : R ≤ T.arrows
⊢ ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
      R ≤
        (Sieve.functorPushforward F
            (Sieve.functorPullback F
              (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                    Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                      ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                    T hT) :
                Sieve (F.obj U)))).arrows

Tactic:
⟨_, H hR, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
R : Presieve.{v_4, u_4} (F.obj U)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R
hle : R ≤ T.arrows
refine :
  map F (functorPullback F R) ≤
    (Sieve.functorPushforward F
        (Sieve.functorPullback F
          (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                  ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                T hT) :
            Sieve (F.obj U)))).arrows
⊢ ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
      R ≤
        (Sieve.functorPushforward F
            (Sieve.functorPullback F
              (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                    Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                      ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                    T hT) :
                Sieve (F.obj U)))).arrows

Tactic:
refine ⟨_, H hR, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
R : Presieve.{v_4, u_4} (F.obj U)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R
hle : R ≤ T.arrows
⊢ map F (functorPullback F R) ≤
    (Sieve.functorPushforward F
        (Sieve.functorPullback F
          (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                  ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                T hT) :
            Sieve (F.obj U)))).arrows

Tactic:
le_trans ?_
      (Presieve.functorPushforward_monotone (Presieve.functorPullback_monotone hle))

Premises used: CategoryTheory.Presieve.functorPullback_monotone, CategoryTheory.Presieve.functorPushforward_monotone, le_trans
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
R : Presieve.{v_4, u_4} (F.obj U)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R
hle : R ≤ T.arrows
refine : map F (functorPullback F R) ≤ functorPushforward F (functorPullback F R)
⊢ map F (functorPullback F R) ≤
    (Sieve.functorPushforward F
        (Sieve.functorPullback F
          (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                  ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                T hT) :
            Sieve (F.obj U)))).arrows

Tactic:
refine le_trans ?_
      (Presieve.functorPushforward_monotone (Presieve.functorPullback_monotone hle))

Premises used: CategoryTheory.Presieve.functorPullback_monotone, CategoryTheory.Presieve.functorPushforward_monotone, le_trans
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
R : Presieve.{v_4, u_4} (F.obj U)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R
hle : R ≤ T.arrows
rw : map F (functorPullback F R) ≤ (Sieve.generate (map F (functorPullback F R))).arrows
⊢ map F (functorPullback F R) ≤ functorPushforward F (functorPullback F R)

Tactic:
rw [← Sieve.arrows_generate_map_eq_functorPushforward]

Premises used: CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward