awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
x : D
⊢ Eq (α :=
    F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)))
      (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) x))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj x) ≫ Functor.map (shiftFunctor D a) (adj.counit.app x)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x))
have w : ∀ (X : C),
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj X))
    (Functor.map (shiftFunctor C a) (adj.unit.app X))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor D a).obj X))
        (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X))
        (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))
Tactic: refine (compatibilityCounit_of_compatibilityUnit adj _ _ (fun X ↦ ?_) _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
E : Type u_4
inst_7 : Category.{v_3, u_4} E
F' : Functor.{v_2, v_3, u_2, u_4} D E
G' : Functor.{v_3, v_2, u_4, u_2} E D
adj' : F' ⊣ G'
inst_8 : HasShift.{v_3, u_4, u_3} E A
inst_9 : F'.CommShift A
inst_10 : G'.CommShift A
inst_11 : adj.CommShift A
inst_12 : adj'.CommShift A
⊢ NatTrans.CommShift (adj.comp adj').unit A
have rw : NatTrans.CommShift
  (adj.unit ≫
    Functor.whiskerRight F.rightUnitor.inv G ≫
      Functor.whiskerRight (F.whiskerLeft adj'.unit) G ≫
        Functor.whiskerRight (F.associator F' G').inv G ≫ ((F ⋙ F').associator G' G).hom)
  A
Tactic: rw [comp_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
E : Type u_4
inst_7 : Category.{v_3, u_4} E
F' : Functor.{v_2, v_3, u_2, u_4} D E
G' : Functor.{v_3, v_2, u_4, u_2} E D
adj' : F' ⊣ G'
inst_8 : HasShift.{v_3, u_4, u_3} E A
inst_9 : F'.CommShift A
inst_10 : G'.CommShift A
inst_11 : adj.CommShift A
inst_12 : adj'.CommShift A
⊢ NatTrans.CommShift (adj.comp adj').counit A
have rw : NatTrans.CommShift
  (((G' ⋙ G).associator F F').inv ≫
    Functor.whiskerRight (G'.associator G F).hom F' ≫
      Functor.whiskerRight (G'.whiskerLeft adj.counit) F' ≫ Functor.whiskerRight G'.rightUnitor.hom F' ≫ adj'.counit)
  A
Tactic: rw [comp_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
Y : D
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) ((G ⋙ F).obj Y) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
    (Functor.map (shiftFunctor D a) (adj.counit.app Y))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F).obj (G.obj Y))
      (NatTrans.app (Iso.inv (Functor.commShiftIso F a)) (G.obj Y))
      (F.map (NatTrans.app (Iso.inv (Functor.commShiftIso G a)) Y) ≫
        adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))
have eq : Eq (α :=
  (shiftFunctor D a ⋙ G ⋙ F).obj Y ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
  (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a)) Y ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))
  (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 D) a)) Y)
Tactic: have eq := NatTrans.shift_app_comm adj.counit a Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
Y : D
eq :
  Eq (α :=
    (shiftFunctor D a ⋙ G ⋙ F).obj Y ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a)) Y ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 D) a)) Y)
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) ((G ⋙ F).obj Y) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
    (Functor.map (shiftFunctor D a) (adj.counit.app Y))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F).obj (G.obj Y))
      (NatTrans.app (Iso.inv (Functor.commShiftIso F a)) (G.obj Y))
      (F.map (NatTrans.app (Iso.inv (Functor.commShiftIso G a)) Y) ≫
        adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))
have eq₁ : Eq (α :=
  F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)
  (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
    (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y)))
  (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
Tactic: simp only [Functor.comp_obj, Functor.id_obj, Functor.commShiftIso_comp_hom_app, assoc,
    Functor.commShiftIso_id_hom_app, comp_id] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
⊢ a + b = 0
have rw : a + b + a = 0 + a
Tactic: rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : a + b + a = 0 + a
⊢ a + b = 0
have rw₁ : a + (b + a) = 0 + a
Tactic: rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : a + b + a = 0 + a
rw₁ : a + (b + a) = 0 + a
⊢ a + b = 0
have rw₂ : a + 0 = 0 + a
Tactic: rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : a + b + a = 0 + a
rw₁ : a + (b + a) = 0 + a
rw₂ : a + 0 = 0 + a
⊢ a + b = 0
have rw₃ : a + 0 = a
Tactic: rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : a + b + a = 0 + a
rw₁ : a + (b + a) = 0 + a
rw₂ : a + 0 = 0 + a
rw₃ : a + 0 = a
⊢ a + b = 0
have rw₄ : a = a
Tactic: rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
⊢ b = -a
have rw : b + a = -a + a
Tactic: rw [← add_left_inj a, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : b + a = -a + a
⊢ b = -a
have rw₁ : 0 = -a + a
Tactic: rw [← add_left_inj a, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : b + a = -a + a
rw₁ : 0 = -a + a
⊢ b = -a
have rw₂ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [← add_left_inj a, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
⊢ a + b = 0
have rw : a + -a = 0
Tactic: rw [eq_neg_of_add_eq_zero_left h, add_neg_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
rw : a + -a = 0
⊢ a + b = 0
have rw₁ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [eq_neg_of_add_eq_zero_left h, add_neg_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
⊢ b = -a
have rw : b + a = -a + a
Tactic: rw [← add_left_inj a, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
rw : b + a = -a + a
⊢ b = -a
have rw₁ : 0 = -a + a
Tactic: rw [← add_left_inj a, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
rw : b + a = -a + a
rw₁ : 0 = -a + a
⊢ b = -a
have rw₂ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [← add_left_inj a, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
⊢ Eq (α := (G ⋙ shiftFunctor C a).obj Y ⟶ (shiftFunctor D a ⋙ G).obj Y) (NatTrans.app (Iso.inv (iso adj a)) Y)
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D b a h))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
        G.map
            (Functor.map (shiftFunctor D a)
              (Functor.map (shiftFunctor D b) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
          G.map
              (Functor.map (shiftFunctor D a)
                (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a b ⋯)) (F.obj (G.obj Y)))) ≫
            G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))
have obtain : ∀ (h : -a + a = 0),
  Eq (α := (G ⋙ shiftFunctor C a).obj Y ⟶ (shiftFunctor D a ⋙ G).obj Y) (NatTrans.app (Iso.inv (iso adj a)) Y)
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a h))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
        G.map
            (Functor.map (shiftFunctor D a)
              (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
          G.map
              (Functor.map (shiftFunctor D a)
                (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj (G.obj Y)))) ≫
            G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))
Tactic: obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a : A
inst_5 : F.CommShift A
Y : D
h : -a + a = 0
| CategoryStruct.comp (Y :=
    G.obj
      (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
        (F.obj
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))))
    (G.map
      (Functor.map (shiftFunctor D a)
        (NatTrans.app (Iso.inv (Functor.commShiftIso F (-a)))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))
    (G.map
      (Functor.map (shiftFunctor D a)
        (NatTrans.app (Iso.hom (Functor.commShiftIso F (-a)))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))
have a₁ : G.map
  (Functor.map (shiftFunctor D a)
    (𝟙 ((F ⋙ shiftFunctor D (-a)).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))
Tactic: rw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj X))
    (Functor.map (shiftFunctor C a) (adj.unit.app X))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor D a).obj X))
        (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)) (NatTrans.app (Iso.hom (iso adj a)) (F.obj X)))
have rw : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
    (shiftFunctor D a ⋙ G).obj (F.obj X))
  (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫
      adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))) ≫
        G.map
            (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a sorry))
              (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))) ≫
          G.map
              (Functor.map (shiftFunctor D a)
                (Functor.map (shiftFunctor D (-a))
                  (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))) ≫
            G.map
                (Functor.map (shiftFunctor D a)
                  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj (G.obj (F.obj X))))) ≫
              G.map (Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj X))
  (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj X)) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj X))
Tactic: rw [← cancel_mono ((RightAdjointCommShift.iso adj a).inv.app _), assoc, assoc,
    Iso.hom_inv_id_app, RightAdjointCommShift.iso_inv_app adj _ _ (neg_add_cancel a)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift 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))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))) ≫
        Functor.map (shiftFunctor D a)
            (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
have a₁ : 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))
  (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
    CategoryStruct.comp (Y :=
      Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D)
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))))
      (Functor.map (𝟭 D) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a sorry))
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
        Functor.map (shiftFunctor D a)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
  (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
Tactic: erw [← NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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 : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift 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))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D)
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))))
        (Functor.map (𝟭 D) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
have a₁ : 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))
  (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
    CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a sorry))
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
        Functor.map (shiftFunctor D a)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
  (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
Tactic: dsimp