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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
Z : D
U : C
iUY : U ⟶ Y
iZU : Z ⟶ G.obj U
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
h :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))
⊢ Sieve.pullback iZU (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
    (K : (a : D) → Set (Sieve a)) Z

Tactic:
apply K.pullback_stable

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- 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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
h :
  ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj U⦄,
    (Sieve.functorPushforward G (G.imageSieve iUW)).arrows f →
      Sieve.pullback f (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
        (K : (a : D) → Set (Sieve a)) Y_1
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))

Tactic:
apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)

Premises used: CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.Functor.functorPushforward_imageSieve_mem
-- 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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
h :
  Sieve.pullback iZU₁
      (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))) ∈
    (K : (a : D) → Set (Sieve a)) Z
⊢ Sieve.pullback (iZU₁ ≫ G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
    (K : (a : D) → Set (Sieve a)) Z

Tactic:
rw [Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
h :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U₁))) ((K : (a : D) → Set (Sieve a)) (G.obj U₁))
    (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))))
⊢ Sieve.pullback iZU₁
      (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))) ∈
    (K : (a : D) → Set (Sieve a)) Z

Tactic:
apply K.pullback_stable

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- 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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ G.map (iU₁U ≫ iUY ≫ iYX) = G.map (iU₁W ≫ iWX)

Tactic:
simp [e₁, e₂]
-- 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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
apply :
  Sieve.functorPushforward G (Sieve.equalizer (iU₁U ≫ iUY ≫ iYX) (iU₁W ≫ iWX)) ≤
    Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U₁))) ((K : (a : D) → Set (Sieve a)) (G.obj U₁))
    (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))))

Tactic:
apply K.superset_covering ?_ (G.functorPushforward_equalizer_mem _
      (iU₁U ≫ iUY ≫ iYX) (iU₁W ≫ iWX) (by simp [e₁, e₂]))

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Functor.functorPushforward_equalizer_mem, CategoryTheory.CategoryStruct.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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
Z : D
U₂ : C
iU₂U₁ : U₂ ⟶ U₁
iZU₂ : Z ⟶ G.obj U₂
e₃ : iU₂U₁ ≫ iU₁U ≫ iUY ≫ iYX = iU₂U₁ ≫ iU₁W ≫ iWX
⊢ ((iZU₂ ≫ G.map iU₂U₁) ≫ G.map iU₁U) ≫ G.map iUY = iZU₂ ≫ G.map (iU₂U₁ ≫ iU₁U ≫ iUY)

Tactic:
simp
-- 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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
Z : D
U₂ : C
iU₂U₁ : U₂ ⟶ U₁
iZU₂ : Z ⟶ G.obj U₂
e₃ : iU₂U₁ ≫ iU₁U ≫ iUY ≫ iYX = iU₂U₁ ≫ iU₁W ≫ iWX
refine : (Sieve.pullback iYX S).arrows (iU₂U₁ ≫ iU₁U ≫ iUY)
⊢ (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))).arrows
    (iZU₂ ≫ G.map iU₂U₁)

Tactic:
refine ⟨_, iU₂U₁ ≫ iU₁U ≫ iUY, iZU₂, ?_, by simp⟩
-- 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 Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
Z : D
U₂ : C
iU₂U₁ : U₂ ⟶ U₁
iZU₂ : Z ⟶ G.obj U₂
e₃ : iU₂U₁ ≫ iU₁U ≫ iUY ≫ iYX = iU₂U₁ ≫ iU₁W ≫ iWX
⊢ (Sieve.pullback iYX S).arrows (iU₂U₁ ≫ iU₁U ≫ iUY)

Tactic:
simpa [e₃] using S.downward_closed hiWX (iU₂U₁ ≫ iU₁W)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.CategoryStruct.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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
h :
  ∀ ⦃Y : D⦄ ⦃f : Y ⟶ G.obj X⦄,
    (Sieve.functorPushforward G S).arrows f →
      Sieve.pullback f (Sieve.functorPushforward G S') ∈ (K : (a : D) → Set (Sieve a)) Y
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S'

Tactic:
apply K.transitive hS

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- 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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
h : Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')) ∈ (K : (a : D) → Set (Sieve a)) Y
⊢ Sieve.pullback (i ≫ G.map g) (Sieve.functorPushforward G S') ∈ (K : (a : D) → Set (Sieve a)) Y

Tactic:
rw [Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
h :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
    (Sieve.pullback (G.map g) (Sieve.functorPushforward G S'))
⊢ Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')) ∈ (K : (a : D) → Set (Sieve a)) Y

Tactic:
apply K.pullback_stable i

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- 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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
    (Sieve.pullback (G.map g) (Sieve.functorPushforward G S'))

Tactic:
K.superset_covering ?_ (H' hg)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- 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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
h : Sieve.functorPushforward G (Sieve.pullback g S') ≤ Sieve.pullback (G.map g) (Sieve.functorPushforward G S')
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
    (Sieve.pullback (G.map g) (Sieve.functorPushforward G S'))

Tactic:
refine K.superset_covering ?_ (H' hg)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- 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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg_1 : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
⊢ (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')).arrows (i' ≫ G.map g')

Tactic:
⟨Z', g' ≫ g, i', hg, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Presieve.functorPushforward
-- 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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg_1 : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
h : (i' ≫ G.map g') ≫ G.map g = i' ≫ G.map (g' ≫ g)
⊢ (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')).arrows (i' ≫ G.map g')

Tactic:
refine ⟨Z', g' ≫ g, i', hg, ?_⟩
-- 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
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg_1 : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
⊢ (i' ≫ G.map g') ≫ G.map g = i' ≫ G.map (g' ≫ g)

Tactic:
simp
-- 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
K : GrothendieckTopology.{v_2, u_2} D
inst_2 : G.LocallyCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
X : C
S : Sieve.{v_1, u_1} X
⊢ S ∈ (G.inducedTopology K : (a : C) → Set (Sieve a)) X ↔
    Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
      (Sieve.functorPushforward G S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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
⊢ G.IsCocontinuous (G.inducedTopology K) K

Tactic:
⟨@fun _ S hS => LocallyCoverDense.functorPushforward_functorPullback_mem ⟨S, hS⟩⟩

Premises used: CategoryTheory.Functor.IsCocontinuous.mk, CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_mem, Subtype.mk
-- 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
K : GrothendieckTopology.{v_2, u_2} D
inst_2 : G.LocallyCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
⊢ CoverPreserving (G.inducedTopology K) K G

Tactic:
⟨@fun _ _ hS => hS⟩

Premises used: CategoryTheory.CoverPreserving.mk