awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Reflective (goal)
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
⊢ NatTrans.app (counit (coreflectorAdjunction j)) (j.obj ((coreflector j).obj X)) =
    j.map ((coreflector j).map (NatTrans.app (counit (coreflectorAdjunction j)) X))
have 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))
Tactic: rw [← cancel_epi (j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X))),
    ← j.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Reflective (hypothesis)
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)
⊢ j.essImage A
have this : 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 _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Reflective (goal)
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)
have refine : Mono (ε.app A ≫ section_ (ε.app A))
Tactic: refine @mono_of_mono _ _ _ _ _ (ε.app A) (section_ (ε.app A)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Reflective (goal)
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 ≫ section_ (ε.app A))
have rw : Mono ((coreflector j ⋙ j).map (section_ (ε.app A)) ≫ ε.app ((coreflector j ⋙ j).obj A))
Tactic: rw [show ε.app A ≫ section_ _ = _ from (ε.naturality (section_ (ε.app A))).symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Reflective (hypothesis)
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)
⊢ j.essImage A
have this₁ : IsIso (ε.app A)
Tactic: haveI := isIso_of_mono_of_isSplitEpi (ε.app A)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Restrict (goal)
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.{v₂ + 1} (α := L.obj X' ⟶ 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)).symm :
          (a : X' ⟶ R.obj Y) → L.obj X' ⟶ Y)
        (f ≫ g) :
      L.obj X' ⟶ Y)
    (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 :
      L.obj X' ⟶ Y)
have apply : 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: apply hiD.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Restrict (goal)
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
⊢ 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)
have 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))
Tactic: apply hiC.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Restrict (goal)
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
⊢ 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))
have suffices : R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)
Tactic: suffices R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g) by
          simp [Trans.trans, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Restrict (goal)
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 : D
⊢ iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)
have dsimp : iD.map
    (hiD.preimage
      (comm1.inv.app (R.obj X) ≫
        ((Equiv.symm (adj.homEquiv (iC.obj (R.obj X)) (iD.obj X)) :
                Equiv.{v₃ + 1, v₄ + 1} (iC.obj (R.obj X) ⟶ R'.obj (iD.obj X)) (L'.obj (iC.obj (R.obj X)) ⟶ iD.obj X)) :
              (a : iC.obj (R.obj X) ⟶ R'.obj (iD.obj X)) → L'.obj (iC.obj (R.obj X)) ⟶ iD.obj X)
            (𝟙 (iC.obj (R.obj X)) ≫ iC.map (𝟙 (R.obj X)) ≫ comm2.inv.app X) ≫
          𝟙 (iD.obj X))) =
  comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)
Tactic: dsimp [restrictFullyFaithful]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Restrict (goal)
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 : D
f : L.obj X ⟶ Y
⊢ ((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y : (a : L.obj X ⟶ Y) → X ⟶ R.obj Y) f =
    hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y)
have apply : iC.map (((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y : (a : L.obj X ⟶ Y) → X ⟶ R.obj Y) f) =
  iC.map (hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y))
Tactic: apply hiC.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Restrict (goal)
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 : D
f : L.obj X ⟶ Y
⊢ iC.map (((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y : (a : L.obj X ⟶ Y) → X ⟶ R.obj Y) f) =
    iC.map (hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y))
have simp : adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) =
  adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y
Tactic: simp only [homEquiv_apply, Functor.comp_obj, Functor.map_comp, map_restrictFullyFaithful_unit_app,
    Functor.id_obj, assoc, Functor.FullyFaithful.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Restrict (goal)
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 : D
f : L.obj X ⟶ Y
⊢ adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y
have e_a : comm2.hom.app (L.obj X) ≫ iC.map (R.map f) = R'.map (iD.map f) ≫ comm2.hom.app Y
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
⊢ IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit
have mp : IsIso t.adj₁.unit → IsIso t.adj₂.counit
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
mp : IsIso t.adj₁.unit → IsIso t.adj₂.counit
⊢ IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit
have mpr : IsIso t.adj₂.counit → IsIso t.adj₁.unit
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
h : F.FullyFaithful
this_1 : F.Full
this : F.Faithful
⊢ IsIso t.adj₂.counit
have rw : IsIso t.adj₁.unit
Tactic: rw [← t.isIso_unit_iff_isIso_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
h : H.FullyFaithful
this_1 : H.Full
this : H.Faithful
⊢ IsIso t.adj₁.unit
have rw : IsIso t.adj₂.counit
Tactic: rw [t.isIso_unit_iff_isIso_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
⊢ t.rightToLeft =
    H.leftUnitor.inv ≫
      whiskerRight t.adj₁.unit H ≫ (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom
have w : ∀ (X : C),
  t.rightToLeft.app X =
    (H.leftUnitor.inv ≫
          whiskerRight t.adj₁.unit H ≫ (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom).app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ t.rightToLeft.app X =
    (H.leftUnitor.inv ≫
          whiskerRight t.adj₁.unit H ≫ (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom).app
      X
have w : G.map (t.rightToLeft.app X) =
  G.map
    ((H.leftUnitor.inv ≫
          whiskerRight t.adj₁.unit H ≫ (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom).app
      X)
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
⊢ t.rightToLeft =
    H.rightUnitor.inv ≫
      inv (H.whiskerLeft t.adj₁.counit) ≫ (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom
have w : ∀ (X : C),
  t.rightToLeft.app X =
    (H.rightUnitor.inv ≫
          inv (H.whiskerLeft t.adj₁.counit) ≫
            (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom).app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ t.rightToLeft.app X =
    (H.rightUnitor.inv ≫
          inv (H.whiskerLeft t.adj₁.counit) ≫
            (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom).app
      X
have w : G.map (t.rightToLeft.app X) =
  G.map
    ((H.rightUnitor.inv ≫
          inv (H.whiskerLeft t.adj₁.counit) ≫
            (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom).app
      X)
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
⊢ t.op.rightToLeft = NatTrans.op t.rightToLeft
have w : ∀ (x : Cᵒᵖ), t.op.rightToLeft.app x = (NatTrans.op t.rightToLeft).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
x : Cᵒᵖ
⊢ t.op.rightToLeft.app x = (NatTrans.op t.rightToLeft).app x
have w : (F.op.leftUnitor.inv ≫
        whiskerRight t.op.adj₁.unit F.op ≫
          (H.op.associator G.op F.op).hom ≫ inv (H.op.whiskerLeft t.op.adj₂.unit) ≫ H.op.rightUnitor.hom).app
    x =
  (NatTrans.op
        (H.rightUnitor.inv ≫
          inv (H.whiskerLeft t.adj₁.counit) ≫
            (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom)).app
    x
Tactic: rw [rightToLeft_eq_units, rightToLeft_eq_counits]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ Epi (t.rightToLeft.app X) ↔ Epi (H.map (t.adj₁.unit.app X))
have rw : Epi (t.rightToLeft.app X ≫ t.adj₂.unit.app (F.obj X)) ↔ Epi (H.map (t.adj₁.unit.app X))
Tactic: rw [← epi_comp_iff_of_isIso _ (t.adj₂.unit.app (F.obj X)), rightToLeft_app_adj₂_unit_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
rw : Epi (t.rightToLeft.app X ≫ t.adj₂.unit.app (F.obj X)) ↔ Epi (H.map (t.adj₁.unit.app X))
⊢ Epi (t.rightToLeft.app X) ↔ Epi (H.map (t.adj₁.unit.app X))
have rw₁ : Epi (H.map (t.adj₁.unit.app X)) ↔ Epi (H.map (t.adj₁.unit.app X))
Tactic: rw [← epi_comp_iff_of_isIso _ (t.adj₂.unit.app (F.obj X)), rightToLeft_app_adj₂_unit_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (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
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ Epi (t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X))
have rw : Epi (t.adj₁.counit.app (H.obj X) ≫ t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X))
Tactic: rw [← epi_comp_iff_of_epi (t.adj₁.counit.app (H.obj X)), adj₁_counit_app_rightToLeft_app]