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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  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) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))
⊢ e₂.inv.app Y =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))
have rw : e₂.inv.app Y =
  Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
    e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))
Tactic: rw [← assoc, ← this, 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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  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) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))
⊢ e₂.inv.app Y =
    Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))
have erw : e₂.inv.app Y =
  Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
    (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y)
Tactic: erw [← e₂.inv.naturality]
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  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) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))
⊢ e₂.inv.app Y =
    Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y)
have rw : e₂.inv.app Y ≫ e₂.hom.app Y =
  (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y)) ≫
    e₂.hom.app Y
Tactic: rw [← cancel_mono (e₂.hom.app _)]
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
⊢ e₁.hom.app X =
    F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
have this : Eq (α :=
  (G ⋙ F).obj (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} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
  (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
  (F.map (e₂.hom.app (F.obj X)) ≫
    e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
Tactic: have := h (F.obj X)
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  Eq (α :=
    (G ⋙ F).obj (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} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (F.map (e₂.hom.app (F.obj X)) ≫
      e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
⊢ e₁.hom.app X =
    F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
have this₁ : Eq (α :=
  F.obj ((G ⋙ shiftFunctor C a).obj (F.obj X)) ⟶
    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 X)))
  (F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
  (e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
Tactic: rw [← cancel_epi (F.map (e₂.inv.app _)), ← assoc, ← F.map_comp, Iso.inv_hom_id_app, F.map_id,
    id_comp] at this
Cleared hypotheses: this
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  Eq (α :=
    F.obj ((G ⋙ shiftFunctor C a).obj (F.obj X)) ⟶
      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 X)))
    (F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
⊢ e₁.hom.app X =
    F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
have rw : e₁.hom.app X = e₁.hom.app X ≫ Functor.map (shiftFunctor D a) (𝟙 (F.obj X))
Tactic: rw [this, dsimp% e₁.hom.naturality_assoc, ← Functor.map_comp, left_triangle_components]
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂ = e₂'
have rw : e₂.symm = e₂'.symm
Tactic: rw [← Iso.symm_eq_iff]
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂.symm = e₂'.symm
have w : ∀ (x : D), e₂.symm.hom.app x = e₂'.symm.hom.app x
Tactic: ext
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x : D
⊢ e₂.symm.hom.app x = e₂'.symm.hom.app x
have w : e₂.inv.app x = e₂'.symm.hom.app x
Tactic: rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h,
    compatibilityUnit_right adj e₁ e₂' 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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x : D
w : e₂.inv.app x = e₂'.symm.hom.app x
⊢ e₂.symm.hom.app x = e₂'.symm.hom.app x
have w₁ : e₂.inv.app x = e₂'.inv.app x
Tactic: rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h,
    compatibilityUnit_right adj e₁ e₂' 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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x : D
w : e₂.inv.app x = e₂'.symm.hom.app x
w₁ : e₂.inv.app x = e₂'.inv.app x
⊢ e₂.symm.hom.app x = e₂'.symm.hom.app x
have w₂ : adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)) ≫
    G.map (e₁.hom.app (G.obj x)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app x)) =
  e₂'.inv.app x
Tactic: rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h,
    compatibilityUnit_right adj e₁ e₂' 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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x : D
w : e₂.inv.app x = e₂'.symm.hom.app x
w₁ : e₂.inv.app x = e₂'.inv.app x
w₂ :
  adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)) ≫
      G.map (e₁.hom.app (G.obj x)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app x)) =
    e₂'.inv.app x
⊢ e₂.symm.hom.app x = e₂'.symm.hom.app x
have w₃ : adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)) ≫
    G.map (e₁.hom.app (G.obj x)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app x)) =
  adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)) ≫
    G.map (e₁.hom.app (G.obj x)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app x))
Tactic: rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h,
    compatibilityUnit_right adj e₁ e₂' 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 : AddMonoid 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
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
⊢ e₁ = e₁'
have w : ∀ (x : C), e₁.hom.app x = e₁'.hom.app x
Tactic: ext
-- 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
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x : C
⊢ e₁.hom.app x = e₁'.hom.app x
have w : F.map (Functor.map (shiftFunctor C a) (adj.unit.app x)) ≫
    F.map (e₂.inv.app (F.obj x)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj x)) =
  e₁'.hom.app x
Tactic: rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
    compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ 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 : AddMonoid 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
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x : C
w :
  F.map (Functor.map (shiftFunctor C a) (adj.unit.app x)) ≫
      F.map (e₂.inv.app (F.obj x)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj x)) =
    e₁'.hom.app x
⊢ e₁.hom.app x = e₁'.hom.app x
have w₁ : F.map (Functor.map (shiftFunctor C a) (adj.unit.app x)) ≫
    F.map (e₂.inv.app (F.obj x)) ≫ adj.counit.app (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)) ≫
    F.map (e₂.inv.app (F.obj x)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj x))
Tactic: rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
    compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]
-- 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
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      G.map ((Functor.CommShift.isoAdd e₁ f₁).hom.app X) ≫ (Functor.CommShift.isoAdd e₂ f₂).hom.app (F.obj X)
have this : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
      (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
      ((F ⋙ G).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
  (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
  (adj.unit.app
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
    G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
Tactic: have := h' (X⟦a⟧)
-- 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
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        ((F ⋙ G).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      G.map ((Functor.CommShift.isoAdd e₁ f₁).hom.app X) ≫ (Functor.CommShift.isoAdd e₂ f₂).hom.app (F.obj X)
have this₁ : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    G.obj
      (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
        (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
  (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
    f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
  (adj.unit.app
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
    G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
Tactic: simp only [← cancel_mono (f₂.inv.app _), assoc, Iso.hom_inv_id_app,
    Functor.id_obj, Functor.comp_obj, comp_id] at this
Cleared hypotheses: this
-- 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
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      G.map ((Functor.CommShift.isoAdd e₁ f₁).hom.app X) ≫ (Functor.CommShift.isoAdd e₂ f₂).hom.app (F.obj X)
have simp : Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
          G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
            G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X)) ≫
              f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
                Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
Tactic: simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoAdd_hom_app,
    Functor.map_comp, assoc, unit_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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
| G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
    G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X))
have a₁ : G.map (𝟙 (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X)))
Tactic: rw [← G.map_comp, Iso.inv_hom_id_app]