awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
e : F ≅ F'
⊢ ∃ (R : F'.RepresentableBy X),
    Eq.{w + 1} (α := F'.obj (op X))
      (((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F'.obj (op X))) : (a : X ⟶ X) → F'.obj (op X)) (𝟙 X) :
        F'.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
          x :
        (fun (X : Type w) ↦ X) (F'.obj (op X)))
have h₁ : Eq.{w + 1} (α := F'.obj (op X))
  ((((h.representableBy.ofIso e).homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F'.obj (op X))) : (a : X ⟶ X) → F'.obj (op X))
      (𝟙 X) :
    F'.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
      x :
    (fun (X : Type w) ↦ X) (F'.obj (op X)))
Tactic: use h.representableBy.ofIso e
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
⊢ F.IsRepresentedBy (X := Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x)
have rw : ∃ (R : F.RepresentableBy Y),
  Eq.{w + 1} (α := F.obj (op Y))
    (((R.homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F.obj (op Y)))
Tactic: rw [iff_exists_representableBy]
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
⊢ ∃ (R : F.RepresentableBy Y),
    Eq.{w + 1} (α := F.obj (op Y))
      (((R.homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))
have h₁ : Eq.{w + 1} (α := F.obj (op Y))
  ((((h.representableBy.ofIsoObj e).homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) :
        (a : Y ⟶ Y) → F.obj (op Y))
      (𝟙 Y) :
    F.obj (op Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x :
    (fun (X : Type w) ↦ X) (F.obj (op Y)))
Tactic: use h.representableBy.ofIsoObj e
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
⊢ F.IsRepresentedBy (X := Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x) ↔
    F.IsRepresentedBy x
have refine : ∀
  (h :
    F.IsRepresentedBy (X := Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x)),
  F.IsRepresentedBy x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.of_isoObj e⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
h :
  F.IsRepresentedBy (X := Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x)
⊢ F.IsRepresentedBy x
have this : x =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv.op) :
      (a : (fun (X : Type w) ↦ X) (F.obj (op Y))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F.obj (op Y)))
Tactic: have : x = F.map e.inv.op (F.map e.hom.op x) := by
    simp [← comp_apply, ← map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : C
h : Retract X Y
F : Functor.{v, v', u, u'} C D
⊢ F.map h.i ≫ F.map h.r = 𝟙 (F.obj X)
have rw : F.map (h.i ≫ h.r) = 𝟙 (F.obj X)
Tactic: rw [← F.map_comp h.i h.r, h.retract, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : C
h : Retract X Y
F : Functor.{v, v', u, u'} C D
rw : F.map (h.i ≫ h.r) = 𝟙 (F.obj X)
⊢ F.map h.i ≫ F.map h.r = 𝟙 (F.obj X)
have rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
Tactic: rw [← F.map_comp h.i h.r, h.retract, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : C
h : Retract X Y
F : Functor.{v, v', u, u'} C D
rw : F.map (h.i ≫ h.r) = 𝟙 (F.obj X)
rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
⊢ F.map h.i ≫ F.map h.r = 𝟙 (F.obj X)
have rw₂ : Eq.{v' + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
Tactic: rw [← F.map_comp h.i h.r, h.retract, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Eq.{v + 1} (α := Quiver.Hom (V := Arrow.{v, u} Cᵒᵖ) (Arrow.mk f.op) (Arrow.mk f.op))
    (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
      (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯))
    (𝟙 (Arrow.mk f.op))
have h₁ : Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.left.{v, u} (Arrow.mk f.op)) (Arrow.left.{v, u} (Arrow.mk f.op)))
  (Arrow.Hom.left
    (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op sorry)
      (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op sorry)))
  (Arrow.Hom.left (𝟙 (Arrow.mk f.op)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h₁ :
  Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.left.{v, u} (Arrow.mk f.op)) (Arrow.left.{v, u} (Arrow.mk f.op)))
    (Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯)))
    (Arrow.Hom.left (𝟙 (Arrow.mk f.op)))
⊢ Eq.{v + 1} (α := Quiver.Hom (V := Arrow.{v, u} Cᵒᵖ) (Arrow.mk f.op) (Arrow.mk f.op))
    (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
      (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯))
    (𝟙 (Arrow.mk f.op))
have h₂ : Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.right.{v, u} (Arrow.mk f.op)) (Arrow.right.{v, u} (Arrow.mk f.op)))
  (Arrow.Hom.right
    (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op sorry)
      (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op sorry)))
  (Arrow.Hom.right (𝟙 (Arrow.mk f.op)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y_1 Z_1 W_1 : C
f_1 : X_1 ⟶ Y_1
g_1 : Z_1 ⟶ W_1
h_1 : RetractArrow f_1 g_1
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) (W := W) f g
⊢ CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
      (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯) =
    𝟙 (Arrow.mk f.unop)
have h₁ : Arrow.Hom.left
    (CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop sorry)
      (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop sorry)) =
  Arrow.Hom.left (𝟙 (Arrow.mk f.unop))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y_1 Z_1 W_1 : C
f_1 : X_1 ⟶ Y_1
g_1 : Z_1 ⟶ W_1
h_1 : RetractArrow f_1 g_1
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) (W := W) f g
h₁ :
  Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk f.unop))
⊢ CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
      (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯) =
    𝟙 (Arrow.mk f.unop)
have h₂ : Arrow.Hom.right
    (CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop sorry)
      (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop sorry)) =
  Arrow.Hom.right (𝟙 (Arrow.mk f.unop))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
      (Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    𝟙 (Arrow.mk (τ.app X))
have h₁ : Arrow.Hom.left
    (CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) sorry)
      (Arrow.homMk (F.map h.r) (G.map h.r) sorry)) =
  Arrow.Hom.left (𝟙 (Arrow.mk (τ.app X)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
τ : F ⟶ G
X Y : C
h : Retract X Y
h₁ :
  Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
        (Arrow.homMk (F.map h.r) (G.map h.r) ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk (τ.app X)))
⊢ CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
      (Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    𝟙 (Arrow.mk (τ.app X))
have h₂ : Arrow.Hom.right
    (CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) sorry)
      (Arrow.homMk (F.map h.r) (G.map h.r) sorry)) =
  Arrow.Hom.right (𝟙 (Arrow.mk (τ.app X)))
Tactic: ext
-- 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 : CompatibilityUnit adj e₁ e₂
Y : D
⊢ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) =
    F.map (e₂.hom.app Y) ≫ e₁.hom.app (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y)
have eq : 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)) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
  (Functor.map (shiftFunctor C a) (adj.unit.app (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₂.hom.app (F.obj (G.obj Y)))
Tactic: have eq := h (G.obj 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
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
eq :
  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)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (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₂.hom.app (F.obj (G.obj Y)))
⊢ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) =
    F.map (e₂.hom.app Y) ≫ e₁.hom.app (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y)
have eq₁ : 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)) ⟶
    G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
  (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
    e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
  (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
Tactic: simp only [← cancel_mono (e₂.inv.app _ ≫ G.map (e₁.inv.app _)),
    assoc, Iso.hom_inv_id_app_assoc, comp_id, ← Functor.map_comp,
    Iso.hom_inv_id_app, Functor.comp_obj, Functor.map_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 : 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
eq :
  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)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
⊢ adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
          e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y))) ≫
        G.map (e₁.hom.app (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))
have a₁ : adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
    G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
  e₂.hom.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: simp only [assoc, ← Functor.map_comp, Iso.inv_hom_id_app_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
eq :
  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)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
⊢ adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.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 a₁ : adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
    G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) 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 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
eq :
  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)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
⊢ adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) 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 Y
have a₁ : adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
    G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
  e₂.hom.app Y ≫
    Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      Functor.map (shiftFunctor C a) (G.map (adj.counit.app Y)) ≫ e₂.inv.app Y
Tactic: dsimp
-- 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 : CompatibilityUnit adj e₁ e₂
Y : D
⊢ 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 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)) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
  (Functor.map (shiftFunctor C a) (adj.unit.app (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₂.hom.app (F.obj (G.obj Y)))
Tactic: have := h (G.obj 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
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)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (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₂.hom.app (F.obj (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 this₁ : 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)) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
Tactic: rw [← cancel_mono (e₂.inv.app _), assoc, assoc, Iso.hom_inv_id_app] at this
Cleared hypotheses: this
-- 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 : CompatibilityUnit adj e₁ e₂
Y : D
this :
  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)) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj (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 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)))
Tactic: erw [comp_id] at this
Cleared hypotheses: this