awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
rw₂ : m + n + a = m + (n + a)
⊢ mn + a = a''
have rw₃ : m + (n + a) = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
a : A
X : C
⊢ NatTrans.app (Iso.hom (F.shiftIso 0 a a ⋯)) X = NatTrans.app (Iso.hom (shiftFunctorZero D A)) ((F.functor a).obj X)
have rw : Eq (α := (F.functor a ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X ⟶ (F.functor a).obj X)
  (NatTrans.app (Iso.hom ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A))) X)
  (NatTrans.app (Iso.hom (shiftFunctorZero D A)) ((F.functor a).obj X))
Tactic: rw [shiftIso_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
a : A
X : C
⊢ NatTrans.app (Iso.inv (F.shiftIso 0 a a ⋯)) X = NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((F.functor a).1 X)
have rw : Eq (α := (F.functor a).obj X ⟶ (F.functor a ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
  (NatTrans.app (Iso.inv ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A))) X)
  (NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((F.functor a).1 X))
Tactic: rw [shiftIso_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw : ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
  (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₁ : (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
  (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₂ : (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
  whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₃ : (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
  whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₃ :
  (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₄ : (G.shiftIso n a a' ha').hom = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₃ :
  (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₄ :
  (G.shiftIso n a a' ha').hom = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₅ : (G.shiftIso n a a' ha').hom =
  whiskerRight (iso a').inv (shiftFunctor D n) ≫
    whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₃ :
  (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₄ :
  (G.shiftIso n a a' ha').hom = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₅ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₆ : (G.shiftIso n a a' ha').hom =
  whiskerRight ((iso a').inv ≫ (iso a').hom) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₃ :
  (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₄ :
  (G.shiftIso n a a' ha').hom = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₅ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₆ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight ((iso a').inv ≫ (iso a').hom) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₇ : (G.shiftIso n a a' ha').hom = whiskerRight (𝟙 (G.functor a')) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₃ :
  (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₄ :
  (G.shiftIso n a a' ha').hom = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₅ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₆ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight ((iso a').inv ≫ (iso a').hom) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₇ : (G.shiftIso n a a' ha').hom = whiskerRight (𝟙 (G.functor a')) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₈ : (G.shiftIso n a a' ha').hom = 𝟙 (G.functor a' ⋙ shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₃ :
  (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₄ :
  (G.shiftIso n a a' ha').hom = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₅ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₆ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight ((iso a').inv ≫ (iso a').hom) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₇ : (G.shiftIso n a a' ha').hom = whiskerRight (𝟙 (G.functor a')) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₈ : (G.shiftIso n a a' ha').hom = 𝟙 (G.functor a' ⋙ shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
have rw₉ : (G.shiftIso n a a' ha').hom = (G.shiftIso n a a' ha').hom
Tactic: rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
⊢ e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)
have rw : (e.hom ≫ e.inv).hom n = 𝟙 (F.functor n)
Tactic: rw [← comp_hom, e.hom_inv_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
rw : (e.hom ≫ e.inv).hom n = 𝟙 (F.functor n)
⊢ e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)
have rw₁ : Hom.hom (𝟙 F) n = 𝟙 (F.functor n)
Tactic: rw [← comp_hom, e.hom_inv_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
rw : (e.hom ≫ e.inv).hom n = 𝟙 (F.functor n)
rw₁ : Hom.hom (𝟙 F) n = 𝟙 (F.functor n)
⊢ e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)
have rw₂ : 𝟙 (F.functor n) = 𝟙 (F.functor n)
Tactic: rw [← comp_hom, e.hom_inv_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
⊢ e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)
have rw : (e.inv ≫ e.hom).hom n = 𝟙 (G.functor n)
Tactic: rw [← comp_hom, e.inv_hom_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
rw : (e.inv ≫ e.hom).hom n = 𝟙 (G.functor n)
⊢ e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)
have rw₁ : Hom.hom (𝟙 G) n = 𝟙 (G.functor n)
Tactic: rw [← comp_hom, e.inv_hom_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
rw : (e.inv ≫ e.hom).hom n = 𝟙 (G.functor n)
rw₁ : Hom.hom (𝟙 G) n = 𝟙 (G.functor n)
⊢ e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)
have rw₂ : 𝟙 (G.functor n) = 𝟙 (G.functor n)
Tactic: rw [← comp_hom, e.inv_hom_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
X : C
⊢ (e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
have rw : (e.hom.hom n ≫ e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
Tactic: rw [← NatTrans.comp_app, hom_inv_id_hom, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
X : C
rw : (e.hom.hom n ≫ e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
⊢ (e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
have rw₁ : NatTrans.app (𝟙 (F.functor n)) X = 𝟙 ((F.functor n).obj X)
Tactic: rw [← NatTrans.comp_app, hom_inv_id_hom, NatTrans.id_app]