awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A : C
inst_3 : IsSplitMono (Y := (reflector i ⋙ i).obj A) (NatTrans.app (unit (reflectorAdjunction i)) A)
η : 𝟭 C ⟶ reflector i ⋙ i := unit (reflectorAdjunction i)
this :
  IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (i.obj ((reflector i).obj A))) (η.app (i.obj ((reflector i).obj A)))
⊢ Epi (η.app A)

Tactic:
have : Epi (η.app A) := by
    refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.app A) ?_
    rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]
    apply epi_comp (η.app (i.obj ((reflector i).obj A)))
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A : C
inst_3 : IsSplitMono (Y := (reflector i ⋙ i).obj A) (NatTrans.app (unit (reflectorAdjunction i)) A)
η : 𝟭 C ⟶ reflector i ⋙ i := unit (reflectorAdjunction i)
this_1 :
  IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (i.obj ((reflector i).obj A))) (η.app (i.obj ((reflector i).obj A)))
this : Epi (η.app A)
⊢ IsIso (η.app A)

Tactic:
haveI := isIso_of_epi_of_isSplitMono (η.app A)
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A : C
inst_3 : IsSplitMono (Y := (reflector i ⋙ i).obj A) (NatTrans.app (unit (reflectorAdjunction i)) A)
η : 𝟭 C ⟶ reflector i ⋙ i := unit (reflectorAdjunction i)
this_1 :
  IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (i.obj ((reflector i).obj A))) (η.app (i.obj ((reflector i).obj A)))
this_2 : Epi (η.app A)
this : IsIso (η.app A)
⊢ i.essImage A

Tactic:
(reflectorAdjunction i).mem_essImage_of_unit_isIso A

Premises used: CategoryTheory.reflectorAdjunction, CategoryTheory.Adjunction.mem_essImage_of_unit_isIso
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A : C
inst_3 : IsSplitMono (Y := (reflector i ⋙ i).obj A) (NatTrans.app (unit (reflectorAdjunction i)) A)
η : 𝟭 C ⟶ reflector i ⋙ i := unit (reflectorAdjunction i)
this_1 :
  IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (i.obj ((reflector i).obj A))) (η.app (i.obj ((reflector i).obj A)))
this_2 : Epi (η.app A)
this : IsIso (η.app A)
⊢ i.essImage A

Tactic:
exact (reflectorAdjunction i).mem_essImage_of_unit_isIso A

Premises used: CategoryTheory.reflectorAdjunction, CategoryTheory.Adjunction.mem_essImage_of_unit_isIso
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A : C
B : D
f : i.obj ((reflector i).obj A) ⟶ i.obj B
⊢ (Equiv.symm (unitCompPartialBijectiveAux A B) : (a : i.obj ((reflector i).obj A) ⟶ i.obj B) → A ⟶ i.obj B) f =
    NatTrans.app (unit (reflectorAdjunction i)) A ≫ f

Tactic:
simp [unitCompPartialBijectiveAux, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.unitCompPartialBijectiveAux
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A B : C
hB : i.essImage B
f : i.obj ((reflector i).obj A) ⟶ B
⊢ (Equiv.symm (unitCompPartialBijective A hB) : (a : i.obj ((reflector i).obj A) ⟶ B) → A ⟶ B) f =
    NatTrans.app (unit (reflectorAdjunction i)) A ≫ f

Tactic:
simp [unitCompPartialBijective, unitCompPartialBijectiveAux_symm_apply]

Premises used: CategoryTheory.unitCompPartialBijective, CategoryTheory.unitCompPartialBijectiveAux_symm_apply
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : i.obj ((reflector i).obj A) ⟶ B
⊢ Eq (α := A ⟶ B')
    ((Equiv.symm (unitCompPartialBijective A hB') : (a : i.obj ((reflector i).obj A) ⟶ B') → A ⟶ B') (f ≫ h) : A ⟶ B')
    ((Equiv.symm (unitCompPartialBijective A hB) : (a : i.obj ((reflector i).obj A) ⟶ B) → A ⟶ B) f ≫ h : A ⟶ B')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
rw :
  f ≫ h =
    (Equiv.symm (unitCompPartialBijective A hB') : (a : i.obj ((reflector i).obj A) ⟶ B') → A ⟶ B')
      ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
        i.obj ((reflector i).obj A) ⟶ B')
rw₁ :
  f ≫ h =
    (Equiv.symm (unitCompPartialBijective A hB) : (a : i.obj ((reflector i).obj A) ⟶ B) → A ⟶ B)
        ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f :
          i.obj ((reflector i).obj A) ⟶ B) ≫
      h
rw₂ rw₃ : f ≫ h = f ≫ h
⊢ Eq (α := i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB' : (a : A ⟶ B') → i.obj ((reflector i).obj A) ⟶ B') (f ≫ h) :
      i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
      i.obj ((reflector i).obj A) ⟶ B')

Tactic:
rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h hB, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.unitCompPartialBijective_symm_natural, Equiv.eq_symm_apply
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : Reflective i
X : i.EssImageSubcategory
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (X.obj (P := i.essImage))) (Y :=
    (reflector i ⋙ i).obj (X.obj (P := i.essImage)))
    (NatTrans.app (unit (reflectorAdjunction i)) (X.obj (P := i.essImage)))

Tactic:
Functor.essImage.unit_isIso X.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.essImage.unit_isIso
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
i : Functor.{v₂, v₁, u₂, u₁} D C
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : Coreflective j
⊢ j.IsLeftAdjoint

Tactic:
⟨_, ⟨coreflectorAdjunction j⟩⟩

Premises used: Nonempty.intro, CategoryTheory.coreflectorAdjunction, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
i : Functor.{v₂, v₁, u₂, u₁} D C
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : Coreflective j
⊢ (coreflector j).IsRightAdjoint

Tactic:
⟨_, ⟨coreflectorAdjunction j⟩⟩

Premises used: Nonempty.intro, CategoryTheory.coreflectorAdjunction, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
X : D
rw :
  CategoryStruct.comp (Y := j.obj ((j ⋙ coreflector j).obj ((coreflector j).obj X)))
      (j.map (NatTrans.app (unit (coreflectorAdjunction j)) ((coreflector j).obj X)))
      (NatTrans.app (counit (coreflectorAdjunction j)) (j.obj ((coreflector j).obj X))) =
    j.map
      (NatTrans.app (unit (coreflectorAdjunction j)) ((coreflector j).obj X) ≫
        (coreflector j).map (NatTrans.app (counit (coreflectorAdjunction j)) X))
⊢ NatTrans.app (counit (coreflectorAdjunction j)) (j.obj ((coreflector j).obj X)) =
    j.map ((coreflector j).map (NatTrans.app (counit (coreflectorAdjunction j)) X))

Tactic:
rw [← cancel_epi (j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X))),
    ← j.map_comp]

Premises used: CategoryTheory.coreflector, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.coreflectorAdjunction, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
X : D
⊢ CategoryStruct.comp (Y := j.obj ((j ⋙ coreflector j).obj ((coreflector j).obj X)))
      (j.map (NatTrans.app (unit (coreflectorAdjunction j)) ((coreflector j).obj X)))
      (NatTrans.app (counit (coreflectorAdjunction j)) (j.obj ((coreflector j).obj X))) =
    j.map
      (NatTrans.app (unit (coreflectorAdjunction j)) ((coreflector j).obj X) ≫
        (coreflector j).map (NatTrans.app (counit (coreflectorAdjunction j)) X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
i : Functor.{v₂, v₁, u₂, u₁} D C
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : Coreflective j
B : C
⊢ IsIso (X := (coreflector j ⋙ j).obj (j.obj B)) (NatTrans.app (counit (coreflectorAdjunction j)) (j.obj B))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
h rwa rwa₁ rwa₂ rwa₃ : j.essImage A
⊢ IsIso (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)

Tactic:
rwa [isIso_counit_app_iff_mem_essImage]

Premises used: CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
⊢ IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))

Tactic:
haveI : IsIso (ε.app (j.obj ((coreflector j).obj A))) :=
    Functor.essImage.counit_isIso ((j.obj_mem_essImage _))
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
this : IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))
⊢ Mono (ε.app A)

Tactic:
@mono_of_mono _ _ _ _ _ (ε.app A) (section_ (ε.app A)) ?_

Premises used: CategoryTheory.mono_of_mono, CategoryTheory.section_, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
this : IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))
refine : Mono (ε.app A ≫ section_ (ε.app A))
⊢ Mono (ε.app A)

Tactic:
refine @mono_of_mono _ _ _ _ _ (ε.app A) (section_ (ε.app A)) ?_

Premises used: CategoryTheory.mono_of_mono, CategoryTheory.section_, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
this : IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))
rw : Mono ((coreflector j ⋙ j).map (section_ (ε.app A)) ≫ ε.app ((coreflector j ⋙ j).obj A))
⊢ Mono (ε.app A ≫ section_ (ε.app A))

Tactic:
rw [show ε.app A ≫ section_ _ = _ from (ε.naturality (section_ (ε.app A))).symm]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.section_, Eq.symm, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
this : IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))
⊢ Mono ((coreflector j ⋙ j).map (section_ (ε.app A)) ≫ ε.app ((coreflector j ⋙ j).obj A))

Tactic:
apply mono_comp _ (ε.app (j.obj ((coreflector j).obj A)))

Premises used: CategoryTheory.coreflector, CategoryTheory.mono_comp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
this_1 : IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))
this : Mono (ε.app A)
⊢ IsIso (ε.app A)

Tactic:
haveI := isIso_of_mono_of_isSplitEpi (ε.app A)
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
this_1 : IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))
this_2 : Mono (ε.app A)
this : IsIso (ε.app A)
⊢ j.essImage A

Tactic:
(coreflectorAdjunction j).mem_essImage_of_counit_isIso A

Premises used: CategoryTheory.Adjunction.mem_essImage_of_counit_isIso, CategoryTheory.coreflectorAdjunction
-- Module: Mathlib.CategoryTheory.Adjunction.Reflective
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
j : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Coreflective j
A : D
inst_3 : IsSplitEpi (X := (coreflector j ⋙ j).obj A) (NatTrans.app (counit (coreflectorAdjunction j)) A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := counit (coreflectorAdjunction j)
this_1 : IsIso (X := (coreflector j ⋙ j).obj (j.obj ((coreflector j).obj A))) (ε.app (j.obj ((coreflector j).obj A)))
this_2 : Mono (ε.app A)
this : IsIso (ε.app A)
⊢ j.essImage A

Tactic:
exact (coreflectorAdjunction j).mem_essImage_of_counit_isIso A

Premises used: CategoryTheory.Adjunction.mem_essImage_of_counit_isIso, CategoryTheory.coreflectorAdjunction
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
⊢ Eq (α := iD.obj (L.obj X') ⟶ iD.obj Y)
    (iD.map
      (((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                    ((comm1.symm.app X').homCongr (Iso.refl (iD.obj Y))))
                  (adj.homEquiv (iC.obj X') (iD.obj Y)))
                (Iso.homCongr (Iso.refl (iC.obj X')) (comm2.app Y)))
              (Equiv.symm hiC.homEquiv)).symm :
          (a : X' ⟶ R.obj Y) → L.obj X' ⟶ Y)
        (f ≫ g)))
    (iD.map
      (L.map f ≫
        ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                    (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                      ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                    (adj.homEquiv (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (Equiv.symm hiC.homEquiv)).symm :
            (a : X ⟶ R.obj Y) → L.obj X ⟶ Y)
          g))

Tactic:
simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm

Premises used: Trans.trans, Eq.symm, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
apply :
  Eq (α := iC.obj X ⟶ iC.obj (R.obj Y))
    (iC.map
      ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
            (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                  ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                (adj.homEquiv (iC.obj X) (iD.obj Y)))
              (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
            (Equiv.symm hiC.homEquiv) :
          (a : L.obj X ⟶ Y) → X ⟶ R.obj Y)
        (f ≫ g)))
    (iC.map
      ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                    ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
                  (adj.homEquiv (iC.obj X) (iD.obj Y')))
                (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y')))
              (Equiv.symm hiC.homEquiv) :
            (a : L.obj X ⟶ Y') → X ⟶ R.obj Y')
          f ≫
        R.map g))
⊢ Eq.{v₁ + 1} (α := X ⟶ R.obj Y)
    ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
            (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                  ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                (adj.homEquiv (iC.obj X) (iD.obj Y)))
              (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
            (Equiv.symm hiC.homEquiv) :
          (a : L.obj X ⟶ Y) → X ⟶ R.obj Y)
        (f ≫ g) :
      X ⟶ R.obj Y)
    ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                    ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
                  (adj.homEquiv (iC.obj X) (iD.obj Y')))
                (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y')))
              (Equiv.symm hiC.homEquiv) :
            (a : L.obj X ⟶ Y') → X ⟶ R.obj Y')
          f ≫
        R.map g :
      X ⟶ R.obj Y)

Tactic:
apply hiC.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
this : R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)
⊢ Eq (α := iC.obj X ⟶ iC.obj (R.obj Y))
    (iC.map
      ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
            (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                  ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                (adj.homEquiv (iC.obj X) (iD.obj Y)))
              (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
            (Equiv.symm hiC.homEquiv) :
          (a : L.obj X ⟶ Y) → X ⟶ R.obj Y)
        (f ≫ g)))
    (iC.map
      ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                    ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
                  (adj.homEquiv (iC.obj X) (iD.obj Y')))
                (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y')))
              (Equiv.symm hiC.homEquiv) :
            (a : L.obj X ⟶ Y') → X ⟶ R.obj Y')
          f ≫
        R.map g))

Tactic:
simp [Trans.trans, this]

Premises used: Trans.trans