awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
K : C
⊢ Eq (α := (F' a).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (m + n)) (L.obj K)) ⟶ (F' a'').obj (L.obj K))
    ((F' a).map
        (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K) ≫
          map (shiftFunctor D n) (NatTrans.app (Iso.inv (commShiftIso L m)) K) ≫
            NatTrans.app (Iso.inv (commShiftIso L n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
          NatTrans.app (Iso.hom (G.shiftIso m a' a'' ha'')) K ≫ (e' a'').inv.app K)
    ((F' a).map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K)) ≫
      (F' a).map (map (shiftFunctor D n) (NatTrans.app (Iso.inv (commShiftIso L m)) K)) ≫
        ((F' a).map (NatTrans.app (Iso.inv (commShiftIso L n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
            (e' a).hom.app
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
              NatTrans.app (Iso.hom (G.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
                (e' a').inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
          (e' a').hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
            NatTrans.app (Iso.hom (G.shiftIso m a' a'' ha'')) K ≫ (e' a'').inv.app K)

Tactic:
simp only [Functor.map_comp, assoc, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
X : C
⊢ NatTrans.app (Iso.hom (F.isoShiftZero M)) (L.obj X) =
    NatTrans.app (Iso.hom (e' 0)) X ≫ NatTrans.app (Iso.hom (G.isoShiftZero M)) X ≫ e.inv.app X

Tactic:
apply induced.isoZero_hom_app_obj

Premises used: CategoryTheory.Functor.ShiftSequence.induced.isoZero_hom_app_obj
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n a a' : M
ha' : n + a = a'
X : C
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (L.obj X) =
    (F.shift a).map (NatTrans.app (Iso.inv (commShiftIso L n)) X) ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' ha')) X ≫ (e' a').inv.app X

Tactic:
apply induced.shiftIso_hom_app_obj

Premises used: CategoryTheory.Functor.ShiftSequence.induced.shiftIso_hom_app_obj
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n : M
X Y : C
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y
a a' : M
h : n + a = a'
dsimp :
  (F.shift a).map (L.map f ≫ NatTrans.app (Iso.hom (commShiftIso L n)) Y) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' h)) (L.obj Y) =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y) ≫ (e' a').inv.app Y
⊢ F.shiftMap (L.map f ≫ NatTrans.app (Iso.hom (commShiftIso L n)) Y) a a' h =
    (e' a).hom.app X ≫ G.shiftMap f a a' h ≫ (e' a').inv.app Y

Tactic:
dsimp [shiftMap]

Premises used: CategoryTheory.Functor.shiftMap
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n : M
X Y : C
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y
a a' : M
h : n + a = a'
rw :
  (F.shift a).map (L.map f) ≫
      CategoryStruct.comp (Y := (F.shift a).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (L.obj Y)))
        ((F.shift a).map (NatTrans.app (Iso.hom (commShiftIso L n)) Y))
        ((F.shift a).map (NatTrans.app (Iso.inv (commShiftIso L n)) Y) ≫
          (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
            NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y) =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y
⊢ (F.shift a).map (L.map f ≫ NatTrans.app (Iso.hom (commShiftIso L n)) Y) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' h)) (L.obj Y) =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y) ≫ (e' a').inv.app Y

Tactic:
rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n : M
X Y : C
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y
a a' : M
h : n + a = a'
nth_rw :
  (F.shift a).map (L.map f) ≫
      (F.shift a).map
          (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (L.obj Y))
            (NatTrans.app (Iso.hom (commShiftIso L n)) Y) (NatTrans.app (Iso.inv (commShiftIso L n)) Y)) ≫
        (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
          NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y
⊢ (F.shift a).map (L.map f) ≫
      CategoryStruct.comp (Y := (F.shift a).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (L.obj Y)))
        ((F.shift a).map (NatTrans.app (Iso.hom (commShiftIso L n)) Y))
        ((F.shift a).map (NatTrans.app (Iso.inv (commShiftIso L n)) Y) ≫
          (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
            NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y) =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y

Tactic:
nth_rw 2 [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n : M
X Y : C
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y
a a' : M
h : n + a = a'
simp :
  (F.shift a).map (L.map f) ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y
⊢ (F.shift a).map (L.map f) ≫
      (F.shift a).map
          (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (L.obj Y))
            (NatTrans.app (Iso.hom (commShiftIso L n)) Y) (NatTrans.app (Iso.inv (commShiftIso L n)) Y)) ≫
        (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
          NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y

Tactic:
simp only [comp_obj, Iso.hom_inv_id_app, map_id, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n : M
X Y : C
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y
a a' : M
h : n + a = a'
rw :
  (F.shift a).map (L.map f) ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y =
    (L ⋙ F' a).map f ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y
⊢ (F.shift a).map (L.map f) ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y

Tactic:
rw [← NatTrans.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n : M
X Y : C
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y =
    (L ⋙ F' a).map f ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' h)) Y ≫ (e' a').inv.app Y

Tactic:
rfl
-- 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.Full
inst_4 : G.Faithful
X : C
S : Sieve.{v_1, u_1} X
mp :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
      (Sieve.functorPushforward G S) →
    ∃ (T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))),
      Sieve.functorPullback G (↑T : Sieve (G.obj X)) = S
mpr :
  (∃ (T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))),
      Sieve.functorPullback G (↑T : Sieve (G.obj X)) = S) →
    Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
      (Sieve.functorPushforward G S)
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
      (Sieve.functorPushforward G S) ↔
    ∃ (T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))),
      Sieve.functorPullback G (↑T : Sieve (G.obj X)) = S

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
K : GrothendieckTopology.{v_2, u_2} D
inst_2 : G.LocallyCoverDense K
inst_3 : G.Full
inst_4 : G.Faithful
X : C
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
    (Sieve.functorPushforward G S)
⊢ ∃ (T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))),
    Sieve.functorPullback G (↑T : Sieve (G.obj X)) = S

Tactic:
⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩

Premises used: CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion, Subtype.mk, Exists.intro, GaloisCoinsertion.u_l_eq
-- 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.Full
inst_4 : G.Faithful
X : C
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
    (Sieve.functorPushforward G S)
⊢ ∃ (T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))),
    Sieve.functorPullback G (↑T : Sieve (G.obj X)) = S

Tactic:
exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
-- 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.Full
inst_4 : G.Faithful
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
    (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))

Tactic:
LocallyCoverDense.functorPushforward_functorPullback_mem T

Premises used: CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_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
K : GrothendieckTopology.{v_2, u_2} D
inst_2 : G.LocallyCoverDense K
inst_3 : G.Full
inst_4 : G.Faithful
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
    (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))

Tactic:
exact LocallyCoverDense.functorPushforward_functorPullback_mem T

Premises used: CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_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 : C
rw : Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X)) ⊤
⊢ 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)}
    ⊤

Tactic:
rw [Set.mem_setOf, Sieve.functorPushforward_top]

Premises used: Set.mem_setOf, CategoryTheory.Sieve.functorPushforward_top
-- 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
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X)) ⊤

Tactic:
K.top_mem _

Premises used: CategoryTheory.GrothendieckTopology.top_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 : C
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X)) ⊤

Tactic:
exact K.top_mem _

Premises used: CategoryTheory.GrothendieckTopology.top_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
h :
  ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj Y⦄,
    (Sieve.functorPushforward G
            (Sieve.functorPullback G
              (↑(Subtype.mk (p := fun (x : Sieve.{v_2, u_2} (G.obj Y)) ↦
                    Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y)) x)
                    (Sieve.pullback (G.map iYX) (Sieve.functorPushforward G S)) ⋯) :
                Sieve (G.obj Y)))).arrows
        f →
      Sieve.pullback f (Sieve.functorPushforward G (Sieve.pullback iYX S)) ∈ (K : (a : D) → Set (Sieve a)) Y_1
⊢ 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 iYX S)

Tactic:
apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem
      ⟨_, K.pullback_stable (G.map iYX) hS⟩)

Premises used: CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Functor.map, 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
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 :
  Sieve.pullback iZU (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
    (K : (a : D) → Set (Sieve a)) Z
⊢ Sieve.pullback (iZU ≫ 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