awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
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
⊢ (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))
        β) =
    β

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
⊢ 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:
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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.rightUnitor_hom_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Functor.whiskerLeft_comp, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.leftUnitor_inv_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.whiskerRight_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.rightUnitor_inv_app, CategoryTheory.Functor.leftUnitor_hom_app, CategoryTheory.Adjunction.right_triangle_components_assoc, CategoryTheory.Functor.whiskerRight_twice, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
h₆ : G.map (adj₁.unit.app (R₁.obj X) ≫ R₁.map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
h₇ : G.map (𝟙 (R₁.obj X)) ≫ β.natTrans.app X = β.natTrans.app X
h₈ : 𝟙 (G.obj (R₁.obj X)) ≫ β.natTrans.app X = β.natTrans.app X
h₉ h₁₀ : β.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

Tactic:
rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.TwoSquare.natTrans, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
d : D
⊢ CategoryStruct.comp (Y := L₂.obj ((H ⋙ R₂).obj d))
      (L₂.map (app ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α) d))
      (adj₂.counit.app (H.obj d)) =
    α.app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
d : D
rw :
  L₂.map ((Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app d) ≫ adj₂.counit.app (H.obj d)
| L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d)

Tactic:
rw [← (mateEquiv adj₁ adj₂).right_inv α]

Premises used: Equiv.right_inv, CategoryTheory.mateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
d : D
conv_lhs :
  L₂.map ((Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app d) ≫
      adj₂.counit.app (H.obj d) =
    app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α) (R₁.obj d) ≫
      H.map (adj₁.counit.app d)
⊢ L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d) =
    app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α) (R₁.obj d) ≫
      H.map (adj₁.counit.app d)

Tactic:
conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]

Premises used: Equiv.right_inv, CategoryTheory.mateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
d : D
⊢ L₂.map ((Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app d) ≫
      adj₂.counit.app (H.obj d) =
    app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α) (R₁.obj d) ≫
      H.map (adj₁.counit.app d)

Tactic:
(mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d)

Premises used: Equiv.symm, CategoryTheory.mateEquiv, CategoryTheory.mateEquiv_counit, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
d : D
⊢ L₂.map ((Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app d) ≫
      adj₂.counit.app (H.obj d) =
    app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α) (R₁.obj d) ≫
      H.map (adj₁.counit.app d)

Tactic:
exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d)

Premises used: Equiv.symm, CategoryTheory.mateEquiv, CategoryTheory.mateEquiv_counit, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
simp :
  G.map (adj₁.unit.app c) ≫
      adj₂.unit.app (G.obj (R₁.obj (L₁.obj c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
⊢ G.map (adj₁.unit.app c) ≫ app ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α) (L₁.obj c) =
    adj₂.unit.app (G.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫ R₂.map (α.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))

Tactic:
simp only [id_obj, comp_obj, mateEquiv, Equiv.coe_fn_mk, comp_app, rightUnitor_inv_app,
    Functor.whiskerLeft_app, associator_hom_app, associator_inv_app, Functor.whiskerRight_app,
    Functor.comp_map, leftUnitor_hom_app, comp_id, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, Equiv.coe_fn_mk, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.rightUnitor_inv_app, CategoryTheory.Functor.leftUnitor_hom_app, CategoryTheory.mateEquiv, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
rw :
  adj₂.unit.app (G.obj c) ≫
      R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
⊢ G.map (adj₁.unit.app c) ≫
      adj₂.unit.app (G.obj (R₁.obj (L₁.obj c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
rw [← adj₂.unit_naturality_assoc]

Premises used: CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
a : R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c))
| R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫ R₂.map (α.natTrans.app (R₁.obj (L₁.obj c)))

Tactic:
rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
slice_lhs :
  adj₂.unit.app (G.obj c) ≫
      R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
slice_lhs 2 3 =>
    rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
rw :
  adj₂.unit.app (G.obj c) ≫
      (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
rw [R₂.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
a : R₂.map (H.map (𝟙 (L₁.obj c)))
| R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c)))

Tactic:
rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
slice_lhs :
  adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c) ≫ R₂.map (H.map (𝟙 (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
⊢ adj₂.unit.app (G.obj c) ≫
      (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
slice_lhs 3 4 =>
    rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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
c : C
⊢ adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c) ≫ R₂.map (H.map (𝟙 (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
simp only [comp_obj, map_id, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
c : C
rw : G.map (adj₁.unit.app c) ≫ (Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app (L₁.obj c)
| G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c)

Tactic:
rw [← (mateEquiv adj₁ adj₂).right_inv α]

Premises used: Equiv.right_inv, CategoryTheory.mateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
c : C
conv_lhs :
  G.map (adj₁.unit.app c) ≫ (Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app (L₁.obj c) =
    adj₂.unit.app (G.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫
      R₂.map
        (app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α)
          (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))
⊢ G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c) =
    adj₂.unit.app (G.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫
      R₂.map
        (app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α)
          (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))

Tactic:
conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]

Premises used: Equiv.right_inv, CategoryTheory.mateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
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₂
c : C
⊢ G.map (adj₁.unit.app c) ≫ (Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app (L₁.obj c) =
    adj₂.unit.app (G.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫
      R₂.map
        (app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α)
          (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))

Tactic:
(unit_mateEquiv adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) c)

Premises used: CategoryTheory.unit_mateEquiv, Equiv.symm, CategoryTheory.mateEquiv, DFunLike.coe