awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map ((i a).inv.app X) ≫
          (s b).map ((i a).hom.app X) ≫
            (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
              F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶ (s (a + b)).obj (F.obj X))
    (NatTrans.app (Iso.inv (i (a + b))) X) (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)

Tactic:
simp only [isoAdd_hom_app, Iso.symm_hom, shiftFunctorAdd_inv_app_obj_of_induced,
          shiftFunctor_of_induced]

Premises used: CategoryTheory.Functor.CommShift.isoAdd_hom_app, CategoryTheory.Iso.symm_hom, CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced, CategoryTheory.shiftFunctor_of_induced
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 ((shiftFunctor C a ⋙ F).obj X)) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map ((i a).inv.app X) ≫
          (s b).map ((i a).hom.app X) ≫
            (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
              F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
rw [← Functor.map_comp_assoc, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 ((shiftFunctor C a ⋙ F).obj X)) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₁ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₂ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₃ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      NatTrans.app (Iso.inv (i (a + b))) X
w₄ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₅ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₆ w₇ :
  Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶ (s (a + b)).obj (F.obj X))
    (NatTrans.app (Iso.inv (i (a + b))) X) (NatTrans.app (Iso.inv (i (a + b))) X)
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
⊢ F.CommShift A

Tactic:
exact
    { commShiftIso := fun a => (i a).symm
      commShiftIso_zero := by
        ext X
        dsimp
        simp only [isoZero_hom_app, shiftFunctorZero_inv_app_obj_of_induced,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
      commShiftIso_add := fun a b => by
        ext X
        dsimp
        simp only [isoAdd_hom_app, Iso.symm_hom, shiftFunctorAdd_inv_app_obj_of_induced,
          shiftFunctor_of_induced]
        rw [← Functor.map_comp_assoc, Iso.inv_hom_id_app]
        dsimp
        rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp] }
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
a : A
⊢ commShiftIso F a = (i a).symm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Shift.Linear
Goal:
R : Type u_1
inst : Ring R
C : Type u_4
inst_1 : Category.{v_1, u_4} C
inst_2 : Preadditive.{v_1, u_4} C
inst_3 : Linear.{u_1, v_1, u_4} R C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : Linear.{u_1, v_2, u_2} R D
M : Type u_3
inst_7 : AddMonoid M
inst_8 : HasShift.{v_1, u_4, u_3} C M
inst_9 : ∀ (n : M), Functor.Linear.{u_1, v_1, u_4, v_1, u_4} R (shiftFunctor C n)
L : Functor.{v_1, v_2, u_4, u_2} C D
W : MorphismProperty.{v_1, u_4} C
inst_10 : L.IsLocalization W
inst_11 : Functor.Linear R L
inst_12 : HasShift.{v_2, u_2, u_3} D M
inst_13 : L.CommShift M
n : M
have :
  ∀ (this : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n)),
    Functor.Linear.{u_1, v_2, u_2, v_2, u_2} R (shiftFunctor D n)
⊢ Functor.Linear.{u_1, v_2, u_2, v_2, u_2} R (shiftFunctor D n)

Tactic:
have : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n) :=
    ⟨(L.commShiftIso n).symm⟩
-- Module: Mathlib.CategoryTheory.Shift.Linear
Goal:
R : Type u_1
inst : Ring R
C : Type u_4
inst_1 : Category.{v_1, u_4} C
inst_2 : Preadditive.{v_1, u_4} C
inst_3 : Linear.{u_1, v_1, u_4} R C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : Linear.{u_1, v_2, u_2} R D
M : Type u_3
inst_7 : AddMonoid M
inst_8 : HasShift.{v_1, u_4, u_3} C M
inst_9 : ∀ (n : M), Functor.Linear.{u_1, v_1, u_4, v_1, u_4} R (shiftFunctor C n)
L : Functor.{v_1, v_2, u_4, u_2} C D
W : MorphismProperty.{v_1, u_4} C
inst_10 : L.IsLocalization W
inst_11 : Functor.Linear R L
inst_12 : HasShift.{v_2, u_2, u_3} D M
inst_13 : L.CommShift M
n : M
this : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n)
rw : Functor.Linear R (shiftFunctor C n ⋙ L)
⊢ Functor.Linear.{u_1, v_2, u_2, v_2, u_2} R (shiftFunctor D n)

Tactic:
rw [← Localization.functor_linear_iff L W R (shiftFunctor C n ⋙ L) (shiftFunctor D n)]

Premises used: CategoryTheory.Localization.functor_linear_iff, CategoryTheory.Functor.comp, CategoryTheory.shiftFunctor
-- Module: Mathlib.CategoryTheory.Shift.Linear
Goal:
R : Type u_1
inst : Ring R
C : Type u_4
inst_1 : Category.{v_1, u_4} C
inst_2 : Preadditive.{v_1, u_4} C
inst_3 : Linear.{u_1, v_1, u_4} R C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : Linear.{u_1, v_2, u_2} R D
M : Type u_3
inst_7 : AddMonoid M
inst_8 : HasShift.{v_1, u_4, u_3} C M
inst_9 : ∀ (n : M), Functor.Linear.{u_1, v_1, u_4, v_1, u_4} R (shiftFunctor C n)
L : Functor.{v_1, v_2, u_4, u_2} C D
W : MorphismProperty.{v_1, u_4} C
inst_10 : L.IsLocalization W
inst_11 : Functor.Linear R L
inst_12 : HasShift.{v_2, u_2, u_3} D M
inst_13 : L.CommShift M
n : M
this : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n)
⊢ Functor.Linear R (shiftFunctor C n ⋙ L)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Linear
Goal:
R : Type u_1
inst : Ring R
C : Type u_4
inst_1 : Category.{v_1, u_4} C
inst_2 : Preadditive.{v_1, u_4} C
inst_3 : Linear.{u_1, v_1, u_4} R C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : Linear.{u_1, v_2, u_2} R D
M : Type u_3
inst_7 : AddMonoid M
inst_8 : HasShift.{v_1, u_4, u_3} C M
inst_9 : ∀ (n : M), Functor.Linear.{u_1, v_1, u_4, v_1, u_4} R (shiftFunctor C n)
L : Functor.{v_1, v_2, u_4, u_2} C D
W : MorphismProperty.{v_1, u_4} C
inst_10 : HasShift W.Localization M
inst_11 : W.Q.CommShift M
inst_12 : Preadditive W.Localization
inst_13 : Linear R W.Localization
inst_14 : Functor.Linear R W.Q
n : M
⊢ Functor.Linear R (C := W.Localization) (shiftFunctor W.Localization n)

Tactic:
linear_of_localization _ W.Q W _

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Shift.linear_of_localization
-- Module: Mathlib.CategoryTheory.Shift.Linear
Goal:
R : Type u_1
inst : Ring R
C : Type u_5
inst_1 : Category.{v_1, u_5} C
inst_2 : Preadditive.{v_1, u_5} C
inst_3 : Linear.{u_1, v_1, u_5} R C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : Linear.{u_1, v_2, u_2} R D
M : Type u_3
inst_7 : AddMonoid M
inst_8 : HasShift.{v_1, u_5, u_3} C M
inst_9 : ∀ (n : M), Functor.Linear.{u_1, v_1, u_5, v_1, u_5} R (shiftFunctor C n)
L : Functor.{v_1, v_2, u_5, u_2} C D
W : MorphismProperty.{v_1, u_5} C
n : M
inst_10 : MorphismProperty.HasLocalization.{u_4, v_1, u_5} W
inst_11 : HasShift.{u_4, u_5, u_3} (MorphismProperty.Localization'.{u_4, v_1, u_5} W) M
inst_12 : Functor.CommShift.{v_1, u_5, u_4, u_5, u_3} (D := MorphismProperty.Localization'.{u_4, v_1, u_5} W) W.Q' M
inst_13 : Preadditive.{u_4, u_5} (MorphismProperty.Localization'.{u_4, v_1, u_5} W)
inst_14 : Linear.{u_1, u_4, u_5} R (MorphismProperty.Localization'.{u_4, v_1, u_5} W)
inst_15 : Functor.Linear.{u_1, v_1, u_5, u_4, u_5} R (D := MorphismProperty.Localization'.{u_4, v_1, u_5} W) W.Q'
⊢ Functor.Linear.{u_1, u_4, u_5, u_4, u_5} R (C := MorphismProperty.Localization'.{u_4, v_1, u_5} W)
    (shiftFunctor (MorphismProperty.Localization'.{u_4, v_1, u_5} W) n)

Tactic:
linear_of_localization _ W.Q' W _

Premises used: CategoryTheory.Shift.linear_of_localization, CategoryTheory.MorphismProperty.Q'
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v₁, u₁, w} C A
inst_3 : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
rw : W.inverseImage (shiftFunctor C a) f
| W f

Tactic:
rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]

Premises used: CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v₁, u₁, w} C A
inst_3 : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
conv_rhs :
  W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) (Functor.map (shiftFunctor C a) f) ↔
    W.inverseImage (shiftFunctor C a) f
⊢ W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) (Functor.map (shiftFunctor C a) f) ↔ W f

Tactic:
conv_rhs => rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]

Premises used: CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v₁, u₁, w} C A
inst_3 : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
⊢ W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) (Functor.map (shiftFunctor C a) f) ↔
    W.inverseImage (shiftFunctor C a) f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
A : Type w
inst_3 : AddMonoid A
inst_4 : HasShift.{v₁, u₁, w} C A
inst_5 : W.IsCompatibleWithShift A
a : A
x x_1 : C
f : x ⟶ x_1
hf : W f
⊢ W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) x) (Functor.map (shiftFunctor C a) f)

Tactic:
simpa only [iff] using hf

Premises used: CategoryTheory.MorphismProperty.IsCompatibleWithShift.iff
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v₁, u₁, w} C A
inst_3 : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
hf : W f
a : A
⊢ W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) (Functor.map (shiftFunctor C a) f)

Tactic:
simpa only [IsCompatibleWithShift.iff W f a] using hf

Premises used: CategoryTheory.MorphismProperty.IsCompatibleWithShift.iff
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
inst_6 : W.IsCompatibleWithShift A
a : A
rw rw₁ : W ≤ W
⊢ W ≤ W.inverseImage (shiftFunctor C a)

Tactic:
rw [MorphismProperty.IsCompatibleWithShift.condition]

Premises used: CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a : A
X : C
⊢ Eq (α := (shiftFunctor D a ⋙ F').obj (L.obj X) ⟶ (F' ⋙ shiftFunctor E a).obj (L.obj X))
    (NatTrans.app (Iso.hom (iso L W F F' a)) (L.obj X))
    (CategoryStruct.comp (Y := F'.obj ((shiftFunctor C a ⋙ L).obj X))
      (F'.map (NatTrans.app (Iso.inv (commShiftIso L a)) X))
      ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        NatTrans.app (Iso.hom (commShiftIso F a)) X ≫ map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)))

Tactic:
simp [commShiftOfLocalization.iso]

Premises used: CategoryTheory.Functor.commShiftOfLocalization.iso
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a : A
X : C
⊢ Eq (α := (F' ⋙ shiftFunctor E a).obj (L.obj X) ⟶ (shiftFunctor D a ⋙ F').obj (L.obj X))
    (NatTrans.app (Iso.inv (iso L W F F' a)) (L.obj X))
    (map (shiftFunctor E a) ((Lifting.iso L W F F').hom.app X) ≫
      CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F).obj X) (NatTrans.app (Iso.inv (commShiftIso F a)) X)
        ((Lifting.iso L W F F').inv.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
          F'.map (NatTrans.app (Iso.hom (commShiftIso L a)) X)))

Tactic:
simp [commShiftOfLocalization.iso]

Premises used: CategoryTheory.Functor.commShiftOfLocalization.iso
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
w :
  Eq (α := shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F' ⟶ F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0)
    (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (Iso.hom (CommShift.isoZero F' A))
⊢ Eq (α := shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F' ≅ F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0)
    (commShiftOfLocalization.iso L W F F' 0) (CommShift.isoZero F' A)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
w :
  ∀ (X : C),
    Eq (α :=
      (shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F').obj (L.obj X) ⟶
        (F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0).obj (L.obj X))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (L.obj X))
      (NatTrans.app (Iso.hom (CommShift.isoZero F' A)) (L.obj X))
⊢ Eq (α := shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F' ⟶ F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0)
    (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (Iso.hom (CommShift.isoZero F' A))

Tactic:
apply natTrans_ext L W

Premises used: CategoryTheory.Localization.natTrans_ext
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
X : C
w :
  Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (L.obj X))
    (NatTrans.app (Iso.hom (CommShift.isoZero F' A)) (L.obj X))
⊢ Eq (α :=
    (shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F').obj (L.obj X) ⟶
      (F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0).obj (L.obj X))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (L.obj X))
    (NatTrans.app (Iso.hom (CommShift.isoZero F' A)) (L.obj X))

Tactic:
dsimp