awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.retracts.rlp ≤ T.rlp

Tactic:
antitone_rlp T.le_retracts

Premises used: CategoryTheory.MorphismProperty.antitone_rlp, CategoryTheory.MorphismProperty.le_retracts
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.retracts.rlp ≤ T.rlp

Tactic:
exact antitone_rlp T.le_retracts

Premises used: CategoryTheory.MorphismProperty.antitone_rlp, CategoryTheory.MorphismProperty.le_retracts
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : T.retracts ≤ T.rlp.llp
⊢ T.rlp ≤ T.retracts.rlp

Tactic:
rw [← le_llp_iff_le_rlp]

Premises used: CategoryTheory.MorphismProperty.le_llp_iff_le_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.retracts ≤ T.rlp.llp

Tactic:
T.retracts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.retracts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.retracts ≤ T.rlp.llp

Tactic:
exact T.retracts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.retracts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
inst_1 : Nonempty ι
A B X_1 Y_1 : C
i : A ⟶ B
p : X_1 ⟶ Y_1
h : HasLiftingProperty i p
X Y : C
i_1 : ι
⊢ HasLiftingProperty i p

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
G : Functor.{v, v_1, u, u_1} C D
inst_2 : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
simp :
  MorphismProperty.rlp (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i)
      (G.asEquivalence.inverse.map (G.map p)) ↔
    MorphismProperty.rlp
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i) p
⊢ HasLiftingProperty (G.map i) (G.map p) ↔ HasLiftingProperty i p

Tactic:
simp only [dsimp% G.asEquivalence.toAdjunction.hasLiftingProperty_iff,
    ← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]

Premises used: CategoryTheory.Adjunction.hasLiftingProperty_iff, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty, Unit, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
G : Functor.{v, v_1, u, u_1} C D
inst_2 : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ MorphismProperty.rlp (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i)
      (G.asEquivalence.inverse.map (G.map p)) ↔
    MorphismProperty.rlp
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i) p

Tactic:
MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.inv.naturality p).symm)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, Eq.symm, CategoryTheory.Iso.inv, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
G : Functor.{v, v_1, u, u_1} C D
inst_2 : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ MorphismProperty.rlp (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i)
      (G.asEquivalence.inverse.map (G.map p)) ↔
    MorphismProperty.rlp
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i) p

Tactic:
exact MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.symm.app _)
      (G.asEquivalence.unitIso.inv.naturality p).symm)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, Eq.symm, CategoryTheory.Iso.inv, CategoryTheory.Arrow.isoMk
-- 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)
X : C
⊢ (isoZero e M F' e').hom.app (L.obj X) =
    NatTrans.app (Iso.hom (e' 0)) X ≫ NatTrans.app (Iso.hom (G.isoShiftZero M)) X ≫ e.inv.app X

Tactic:
NatTrans.congr_app (((whiskeringLeft C D A).obj L).map_preimage _) X

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.whiskeringLeft, CategoryTheory.Functor.obj, CategoryTheory.Functor.map_preimage
-- 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'
⊢ shiftFunctor D n ⋙ F' a ≅ F' a'

Tactic:
exact ((whiskeringLeft C D A).obj L).preimageIso ((Functor.associator _ _ _).symm ≪≫
    isoWhiskerRight (L.commShiftIso n).symm _ ≪≫
    Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (e' a) ≪≫
    G.shiftIso n a a' ha' ≪≫ (e' a').symm)

Premises used: CategoryTheory.Functor.associator, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.preimageIso, CategoryTheory.Functor.shiftIso, CategoryTheory.Iso.trans, CategoryTheory.Functor.whiskeringLeft, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Functor.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
G : Functor.{v_1, v_3, u_1, u_3} C A
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
⊢ ((L.associator (shiftFunctor D n) (F' a)).symm ≪≫
            isoWhiskerRight (Iso.symm (commShiftIso L n)) (F' a) ≪≫
              associator (shiftFunctor C n) L (F' a) ≪≫
                isoWhiskerLeft (shiftFunctor C n) (e' a) ≪≫ G.shiftIso n a a' ha' ≪≫ (e' a').symm).hom.app
      X =
    (F' 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:
simp
-- 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
a : M
w :
  Eq (α := shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a ⟶ F' a) (Iso.hom (induced.shiftIso L G M F' e' 0 a a ⋯))
    (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor))
⊢ Eq (α := shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a ≅ F' a) (induced.shiftIso L G M F' e' 0 a a ⋯)
    (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)

Tactic:
ext1
-- 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
a : M
w :
  Eq (α :=
    obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ 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' 0 a a ⋯)))
    (map (obj (whiskeringLeft C D A) L) (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))
⊢ Eq (α := shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a ⟶ F' a) (Iso.hom (induced.shiftIso L G M F' e' 0 a a ⋯))
    (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor))

Tactic:
apply ((whiskeringLeft C D A).obj L).map_injective

Premises used: CategoryTheory.Functor.whiskeringLeft, CategoryTheory.Functor.map_injective, CategoryTheory.Functor.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
a : M
w :
  ∀ (K : C),
    Eq (α :=
      (obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ 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' 0 a a ⋯))) K)
      (NatTrans.app
        (map (obj (whiskeringLeft C D A) L)
          (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))
        K)
⊢ Eq (α :=
    obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ 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' 0 a a ⋯)))
    (map (obj (whiskeringLeft C D A) L) (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))

Tactic:
ext K
-- 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
a : M
K : C
w :
  Eq (α :=
    (F' a).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0) (L.obj K)) ⟶ (F' a).obj (L.obj K))
    (NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' 0 a a ⋯)) (L.obj K))
    ((F' a).map (NatTrans.app (Iso.hom (shiftFunctorZero D M)) (L.obj K)) ≫ 𝟙 ((F' a).obj (L.obj K)))
⊢ Eq (α :=
    (obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ 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' 0 a a ⋯))) K)
    (NatTrans.app
      (map (obj (whiskeringLeft C D A) L)
        (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))
      K)

Tactic:
dsimp
-- 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
a : M
K : C
⊢ Eq (α :=
    (F' a).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0) (L.obj K)) ⟶ (F' a).obj (L.obj K))
    (NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' 0 a a ⋯)) (L.obj K))
    ((F' a).map (NatTrans.app (Iso.hom (shiftFunctorZero D M)) (L.obj K)) ≫ 𝟙 ((F' a).obj (L.obj K)))

Tactic:
simp only [induced.shiftIso_hom_app_obj, shiftIso_zero_hom_app, id_obj,
      NatTrans.naturality, comp_map, Iso.hom_inv_id_app_assoc,
      comp_id, ← Functor.map_comp, L.commShiftIso_zero, CommShift.isoZero_inv_app, assoc,
      Iso.inv_hom_id_app, Functor.map_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.shiftIso_zero_hom_app, CategoryTheory.Functor.ShiftSequence.induced.shiftIso_hom_app_obj, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.CommShift.isoZero_inv_app, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- 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''
w :
  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''))
⊢ 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'')

Tactic:
ext1
-- 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''
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'' ⋯)))
    (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'')))
⊢ 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''))

Tactic:
apply ((whiskeringLeft C D A).obj L).map_injective

Premises used: CategoryTheory.Functor.whiskeringLeft, CategoryTheory.Functor.map_injective, CategoryTheory.Functor.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 a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
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'' ⋯))) 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)
⊢ 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'')))

Tactic:
ext K
-- 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
w :
  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)
⊢ 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)

Tactic:
dsimp