awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
X : Cᵒᵖ
t : (obj (cones J C) (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
erw :
  Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j ≫ G.map (K.map f)))
erw₁ :
  Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (map (unop (obj (Functor.op (const J)) X)) f ≫ t.app j'))
⊢ Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j)) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j)) (F.obj (unop X) ⟶ K.obj j)) :
          (a : unop X ⟶ G.obj (K.obj j)) → F.obj (unop X) ⟶ K.obj j)
        (t.app j) ≫
      K.map f)
have erw₂ : Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
  (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j') :
    F.obj (unop X) ⟶ K.obj j')
  (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (map (unop (obj (Functor.op (const J)) X)) f ≫ t.app j') :
    F.obj (unop X) ⟶ K.obj j')
Tactic: erw [← adj.homEquiv_naturality_right_symm, ← t.naturality, Category.id_comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
⊢ (fun (β : TwoSquare R₁ H G R₂) ↦
        TwoSquare.mk G L₁ L₂ H
          ((G ⋙ L₂).leftUnitor.inv ≫
            whiskerRight adj₁.unit (G ⋙ L₂) ≫
              ((L₁ ⋙ R₁).associator G L₂).inv ≫
                whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                  whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                    whiskerRight (L₁.associator H R₂).inv L₂ ≫
                      ((L₁ ⋙ H).associator R₂ L₂).hom ≫ (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
      ((fun (α : TwoSquare G L₁ L₂ H) ↦
          TwoSquare.mk R₁ H G R₂
            ((R₁ ⋙ G).rightUnitor.inv ≫
              (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                  R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                    R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                      R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                        (R₁.associator L₁ (H ⋙ R₂)).inv ≫ whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
        α) =
    α
have h : ∀ (X : C),
  app
      (natTrans
        ((fun (β : TwoSquare R₁ H G R₂) ↦
            TwoSquare.mk G L₁ L₂ H
              ((G ⋙ L₂).leftUnitor.inv ≫
                whiskerRight adj₁.unit (G ⋙ L₂) ≫
                  ((L₁ ⋙ R₁).associator G L₂).inv ≫
                    whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                      whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                        whiskerRight (L₁.associator H R₂).inv L₂ ≫
                          ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                            (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
          ((fun (α : TwoSquare G L₁ L₂ H) ↦
              TwoSquare.mk R₁ H G R₂
                ((R₁ ⋙ G).rightUnitor.inv ≫
                  (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                    (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                      R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                        R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                          R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                            (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                              whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
            α)))
      X =
    α.natTrans.app X
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X : C
⊢ app
      (natTrans
        ((fun (β : TwoSquare R₁ H G R₂) ↦
            TwoSquare.mk G L₁ L₂ H
              ((G ⋙ L₂).leftUnitor.inv ≫
                whiskerRight adj₁.unit (G ⋙ L₂) ≫
                  ((L₁ ⋙ R₁).associator G L₂).inv ≫
                    whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                      whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                        whiskerRight (L₁.associator H R₂).inv L₂ ≫
                          ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                            (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
          ((fun (α : TwoSquare G L₁ L₂ H) ↦
              TwoSquare.mk R₁ H G R₂
                ((R₁ ⋙ G).rightUnitor.inv ≫
                  (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                    (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                      R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                        R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                          R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                            (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                              whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
            α)))
      X =
    α.natTrans.app X
have h : L₂.map (G.map (adj₁.unit.app X)) ≫ α.natTrans.app (R₁.obj (L₁.obj X)) ≫ H.map (adj₁.counit.app (L₁.obj X)) =
  α.natTrans.app X
Tactic: simp only [comp_obj, whiskerLeft_comp, whiskerLeft_twice, assoc, Iso.hom_inv_id_assoc,
      whiskerRight_comp, comp_app, id_obj, leftUnitor_inv_app, Functor.whiskerRight_app,
      Functor.comp_map, associator_inv_app, associator_hom_app, map_id, Functor.whiskerLeft_app,
      rightUnitor_inv_app, leftUnitor_hom_app, rightUnitor_hom_app, comp_id, id_comp,
      counit_naturality, counit_naturality_assoc, left_triangle_components_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X : C
⊢ L₂.map (G.map (adj₁.unit.app X)) ≫ α.natTrans.app (R₁.obj (L₁.obj X)) ≫ H.map (adj₁.counit.app (L₁.obj X)) =
    α.natTrans.app X
have h : α.natTrans.app X ≫ 𝟙 (H.obj (L₁.obj X)) = α.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, α.natTrans.naturality, Functor.comp_map, assoc, ← H.map_comp,
      left_triangle_components, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
⊢ (fun (α : TwoSquare G L₁ L₂ H) ↦
        TwoSquare.mk R₁ H G R₂
          ((R₁ ⋙ G).rightUnitor.inv ≫
            (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
              (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                  R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                    R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                      (R₁.associator L₁ (H ⋙ R₂)).inv ≫ whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
      ((fun (β : TwoSquare R₁ H G R₂) ↦
          TwoSquare.mk G L₁ L₂ H
            ((G ⋙ L₂).leftUnitor.inv ≫
              whiskerRight adj₁.unit (G ⋙ L₂) ≫
                ((L₁ ⋙ R₁).associator G L₂).inv ≫
                  whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                    whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                      whiskerRight (L₁.associator H R₂).inv L₂ ≫
                        ((L₁ ⋙ H).associator R₂ L₂).hom ≫ (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
        β) =
    β
have h : ∀ (X : D),
  app
      (natTrans
        ((fun (α : TwoSquare G L₁ L₂ H) ↦
            TwoSquare.mk R₁ H G R₂
              ((R₁ ⋙ G).rightUnitor.inv ≫
                (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                  (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                    R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                      R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                        R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                          (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                            whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
          ((fun (β : TwoSquare R₁ H G R₂) ↦
              TwoSquare.mk G L₁ L₂ H
                ((G ⋙ L₂).leftUnitor.inv ≫
                  whiskerRight adj₁.unit (G ⋙ L₂) ≫
                    ((L₁ ⋙ R₁).associator G L₂).inv ≫
                      whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                        whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                          whiskerRight (L₁.associator H R₂).inv L₂ ≫
                            ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                              (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
            β)))
      X =
    β.natTrans.app X
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
⊢ app
      (natTrans
        ((fun (α : TwoSquare G L₁ L₂ H) ↦
            TwoSquare.mk R₁ H G R₂
              ((R₁ ⋙ G).rightUnitor.inv ≫
                (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                  (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                    R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                      R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                        R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                          (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                            whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
          ((fun (β : TwoSquare R₁ H G R₂) ↦
              TwoSquare.mk G L₁ L₂ H
                ((G ⋙ L₂).leftUnitor.inv ≫
                  whiskerRight adj₁.unit (G ⋙ L₂) ≫
                    ((L₁ ⋙ R₁).associator G L₂).inv ≫
                      whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                        whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                          whiskerRight (L₁.associator H R₂).inv L₂ ≫
                            ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                              (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
            β)))
      X =
    β.natTrans.app X
have h : G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
  β.natTrans.app X
Tactic: simp only [comp_obj, whiskerRight_comp, whiskerRight_twice, assoc, Iso.inv_hom_id_assoc,
      whiskerLeft_comp, comp_app, id_obj, rightUnitor_inv_app, Functor.whiskerLeft_app,
      associator_hom_app, associator_inv_app, Functor.whiskerRight_app, leftUnitor_inv_app, map_id,
      Functor.comp_map, rightUnitor_hom_app, leftUnitor_hom_app, comp_id, id_comp,
      unit_naturality_assoc, right_triangle_components_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h : (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
  β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₁ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
  β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₂ : G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
  β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₂ :
  G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₃ : G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X) ≫ β.natTrans.app X = β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₂ :
  G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₃ : G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X) ≫ β.natTrans.app X = β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₄ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₂ :
  G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₃ : G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X) ≫ β.natTrans.app X = β.natTrans.app X
h₄ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₅ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ G.map (R₁.map (adj₁.counit.app X))) ≫ β.natTrans.app X = β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₂ :
  G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₃ : G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X) ≫ β.natTrans.app X = β.natTrans.app X
h₄ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
h₅ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ G.map (R₁.map (adj₁.counit.app X))) ≫ β.natTrans.app X = β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₆ : G.map (adj₁.unit.app (R₁.obj X) ≫ R₁.map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]