awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a : A
hτ : CommShiftCore τ a
X : C
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X))
have rw : Eq (α :=
  Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
  (Functor.map (shiftFunctor D a) (τ.app X))
  (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X)))
Tactic: rw [← hτ.shift_app_comm, Iso.inv_hom_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a : A
hτ : CommShiftCore τ a
X : C
rw :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X)))
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X))
have rw₁ : Eq (α :=
  Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
  (Functor.map (shiftFunctor D a) (τ.app X)) (Functor.map (shiftFunctor D a) (τ.app X))
Tactic: rw [← hτ.shift_app_comm, Iso.inv_hom_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F₁ ⟶ F₂ ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0)
    (Iso.hom (Functor.commShiftIso F₁ 0) ≫ Functor.whiskerRight τ (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0))
    (Functor.whiskerLeft (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0) τ ≫ Iso.hom (Functor.commShiftIso F₂ 0))
have w : ∀ (X : C),
  Eq (α :=
    (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
    (app (Iso.hom (Functor.commShiftIso F₁ 0) ≫ Functor.whiskerRight τ (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0)) X)
    (app (Functor.whiskerLeft (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0) τ ≫ Iso.hom (Functor.commShiftIso F₂ 0)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F₁ ⟶ F₂ ⋙ shiftFunctor D (a + b))
    (Iso.hom (Functor.commShiftIso F₁ (a + b)) ≫ Functor.whiskerRight τ (shiftFunctor D (a + b)))
    (Functor.whiskerLeft (shiftFunctor C (a + b)) τ ≫ Iso.hom (Functor.commShiftIso F₂ (a + b)))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C (a + b) ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor D (a + b)).obj X)
    (app (Iso.hom (Functor.commShiftIso F₁ (a + b)) ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))) X)
    (app (Functor.whiskerLeft (shiftFunctor C (a + b)) τ ≫ Iso.hom (Functor.commShiftIso F₂ (a + b))) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (hypothesis)
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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor D (a + b)).obj X)
    (app (Iso.hom (Functor.commShiftIso F₁ (a + b)) ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))) X)
    (app (Functor.whiskerLeft (shiftFunctor C (a + b)) τ ≫ Iso.hom (Functor.commShiftIso F₂ (a + b))) X)
have this : Eq (α :=
  Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F₁.obj X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
  (Functor.map (shiftFunctor D a ⋙ shiftFunctor D b) (τ.app X) ≫ app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X))
  (app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
Tactic: have := (shiftFunctorAdd D a b).inv.naturality (τ.app X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
this :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (Functor.map (shiftFunctor D a ⋙ shiftFunctor D b) (τ.app X) ≫ app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X))
    (app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor D (a + b)).obj X)
    (app (Iso.hom (Functor.commShiftIso F₁ (a + b)) ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))) X)
    (app (Functor.whiskerLeft (shiftFunctor C (a + b)) τ ≫ Iso.hom (Functor.commShiftIso F₂ (a + b))) X)
have w : Eq (α :=
  F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
  (app (Iso.hom (Functor.commShiftIso F₁ (a + b))) X ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
  (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
    app (Iso.hom (Functor.commShiftIso F₂ (a + b))) X)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : CommShift τ A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X))
have rw : Eq (α :=
  Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
  (Functor.map (shiftFunctor D a) (τ.app X))
  (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X)))
Tactic: rw [← shift_app_comm, Iso.inv_hom_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : CommShift τ A
a : A
X : C
rw :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X)))
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X))
have rw₁ : Eq (α :=
  Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
  (Functor.map (shiftFunctor D a) (τ.app X)) (Functor.map (shiftFunctor D a) (τ.app X))
Tactic: rw [← shift_app_comm, Iso.inv_hom_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : 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} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
⊢ Eq (α := shiftFunctor C a ⋙ F₂ ⟶ F₁ ⋙ shiftFunctor D a)
    (Iso.hom (Functor.commShiftIso F₂ a) ≫ Functor.whiskerRight e.inv (shiftFunctor D a))
    (Functor.whiskerLeft (shiftFunctor C a) e.inv ≫ Iso.hom (Functor.commShiftIso F₁ a))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C a ⋙ F₂).obj X ⟶ (F₁ ⋙ shiftFunctor D a).obj X)
    (app (Iso.hom (Functor.commShiftIso F₂ a) ≫ Functor.whiskerRight e.inv (shiftFunctor D a)) X)
    (app (Functor.whiskerLeft (shiftFunctor C a) e.inv ≫ Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : 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} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
⊢ Eq (α := (shiftFunctor C a ⋙ F₂).obj X ⟶ (F₁ ⋙ shiftFunctor D a).obj X)
    (app (Iso.hom (Functor.commShiftIso F₂ a) ≫ Functor.whiskerRight e.inv (shiftFunctor D a)) X)
    (app (Functor.whiskerLeft (shiftFunctor C a) e.inv ≫ Iso.hom (Functor.commShiftIso F₁ a)) X)
have w : Eq (α :=
  F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
  (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
  (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : 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} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
⊢ Eq (α :=
    F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
have w : Eq (α :=
  F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
  (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
    app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
  (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
    e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc,
    ← Functor.map_comp, e.hom_inv_id_app, Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : 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} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
w :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
⊢ Eq (α :=
    F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
have w₁ : Eq (α :=
  F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
  (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
    app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc,
    ← Functor.map_comp, e.hom_inv_id_app, Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : 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} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
w :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₁ :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
⊢ Eq (α :=
    F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
have w₂ : Eq (α :=
  F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫
    Functor.map (shiftFunctor D a) (e.hom.app X) ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc,
    ← Functor.map_comp, e.hom_inv_id_app, Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : 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} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
w :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₁ :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₂ :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫
      Functor.map (shiftFunctor D a) (e.hom.app X) ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
⊢ Eq (α :=
    F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
have w₃ : Eq (α :=
  F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (e.hom.app X ≫ e.inv.app X))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc,
    ← Functor.map_comp, e.hom_inv_id_app, Functor.map_id, Category.comp_id]