awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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''
⊢ Eq (α := shiftFunctor D (m + n) ⋙ F' a ≅ F' a'') (induced.shiftIso L G M F' e' (m + n) a a'' ⋯)
    (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
      associator (shiftFunctor D m) (shiftFunctor D n) (F' a) ≪≫
        isoWhiskerLeft (shiftFunctor D m) (induced.shiftIso L G M F' e' n a a' ha') ≪≫
          induced.shiftIso L G M F' e' m a' a'' ha'')
have w : Eq (α := shiftFunctor D (m + n) ⋙ F' a ⟶ F' a'') (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' sorry))
  (Iso.hom
    (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
      associator (shiftFunctor D m) (shiftFunctor D n) (F' a) ≪≫
        isoWhiskerLeft (shiftFunctor D m) (induced.shiftIso L G M F' e' n a a' ha') ≪≫
          induced.shiftIso L G M F' e' m a' a'' ha''))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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''
⊢ Eq (α := shiftFunctor D (m + n) ⋙ F' a ⟶ F' a'') (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' ⋯))
    (Iso.hom
      (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
        associator (shiftFunctor D m) (shiftFunctor D n) (F' a) ≪≫
          isoWhiskerLeft (shiftFunctor D m) (induced.shiftIso L G M F' e' n a a' ha') ≪≫
            induced.shiftIso L G M F' e' m a' a'' ha''))
have w : Eq (α :=
  obj (obj (whiskeringLeft C D A) L) (shiftFunctor D (m + n) ⋙ F' a) ⟶ obj (obj (whiskeringLeft C D A) L) (F' a''))
  (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' sorry)))
  (map (obj (whiskeringLeft C D A) L)
    (Iso.hom
      (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
        associator (shiftFunctor D m) (shiftFunctor D n) (F' a) ≪≫
          isoWhiskerLeft (shiftFunctor D m) (induced.shiftIso L G M F' e' n a a' ha') ≪≫
            induced.shiftIso L G M F' e' m a' a'' ha'')))
Tactic: apply ((whiskeringLeft C D A).obj L).map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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''
⊢ Eq (α :=
    obj (obj (whiskeringLeft C D A) L) (shiftFunctor D (m + n) ⋙ F' a) ⟶ obj (obj (whiskeringLeft C D A) L) (F' a''))
    (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' ⋯)))
    (map (obj (whiskeringLeft C D A) L)
      (Iso.hom
        (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
          associator (shiftFunctor D m) (shiftFunctor D n) (F' a) ≪≫
            isoWhiskerLeft (shiftFunctor D m) (induced.shiftIso L G M F' e' n a a' ha') ≪≫
              induced.shiftIso L G M F' e' m a' a'' ha'')))
have w : ∀ (K : C),
  Eq (α :=
    (obj (obj (whiskeringLeft C D A) L) (shiftFunctor D (m + n) ⋙ F' a)).obj K ⟶
      (obj (obj (whiskeringLeft C D A) L) (F' a'')).obj K)
    (NatTrans.app (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' sorry))) K)
    (NatTrans.app
      (map (obj (whiskeringLeft C D A) L)
        (Iso.hom
          (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
            associator (shiftFunctor D m) (shiftFunctor D n) (F' a) ≪≫
              isoWhiskerLeft (shiftFunctor D m) (induced.shiftIso L G M F' e' n a a' ha') ≪≫
                induced.shiftIso L G M F' e' m a' a'' ha'')))
      K)
Tactic: ext K
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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 (α :=
    (obj (obj (whiskeringLeft C D A) L) (shiftFunctor D (m + n) ⋙ F' a)).obj K ⟶
      (obj (obj (whiskeringLeft C D A) L) (F' a'')).obj K)
    (NatTrans.app (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' ⋯))) K)
    (NatTrans.app
      (map (obj (whiskeringLeft C D A) L)
        (Iso.hom
          (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
            associator (shiftFunctor D m) (shiftFunctor D n) (F' a) ≪≫
              isoWhiskerLeft (shiftFunctor D m) (induced.shiftIso L G M F' e' n a a' ha') ≪≫
                induced.shiftIso L G M F' e' m a' a'' ha'')))
      K)
have w : NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' sorry)) (L.obj K) =
  (F' a).map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K)) ≫
    𝟙
        ((F' a).obj
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)))) ≫
      NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' n a a' ha'))
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)) ≫
        NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' m a' a'' ha'')) (L.obj K)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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
⊢ NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' ⋯)) (L.obj K) =
    (F' a).map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K)) ≫
      𝟙
          ((F' a).obj
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)))) ≫
        NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' n a a' ha'))
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)) ≫
          NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' m a' a'' ha'')) (L.obj K)
have w : 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)) ≫
    (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)) ≫
        (F' a).map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C m n)) K)) ≫
          (F' a).map (L.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) 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)) ≫
    NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' n a a' ha'))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)) ≫
      (F' a').map (NatTrans.app (Iso.inv (commShiftIso L 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 [id_comp, induced.shiftIso_hom_app_obj,
      G.shiftIso_add_hom_app n m a a' a'' ha' ha'', L.commShiftIso_add,
      comp_obj, CommShift.isoAdd_inv_app, (F' a).map_comp, assoc,
      ← (e' a).hom.naturality_assoc, comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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.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
have 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
Tactic: dsimp [shiftMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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 ≫ 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
have 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
Tactic: rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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) ≫
      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
have 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
Tactic: nth_rw 2 [← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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) ≫
      (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
have 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
Tactic: simp only [comp_obj, Iso.hom_inv_id_app, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
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 =
    (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
have 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
Tactic: rw [← NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ 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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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_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)}
    ⊤
have rw : Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X)) ⊤
Tactic: rw [Set.mem_setOf, Sieve.functorPushforward_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ 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)
have 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)) sorry) :
              Sieve (G.obj Y)))).arrows
      f →
    Sieve.pullback f (Sieve.functorPushforward G (Sieve.pullback iYX S)) ∈ (K : (a : D) → Set (Sieve a)) Y_1
Tactic: apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem
      ⟨_, K.pullback_stable (G.map iYX) hS⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ Sieve.pullback (iZU ≫ G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)) ∈ (K : (a : D) → Set (Sieve a)) Z
have h : Sieve.pullback iZU (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
  (K : (a : D) → Set (Sieve a)) Z
Tactic: rw [Sieve.pullback_comp]