awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ (a : X ⟶ Y), L.map a = f
have h₁ : L.map
    (((h.homEquiv X (L.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (L.obj X ⟶ L.obj Y) (X ⟶ R.obj (L.obj Y))) :
          (a : L.obj X ⟶ L.obj Y) → X ⟶ R.obj (L.obj Y))
        f ≫
      section_ (h.unit.app Y)) =
  f
Tactic: use ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y))
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map
      (((h.homEquiv X (L.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (L.obj X ⟶ L.obj Y) (X ⟶ R.obj (L.obj Y))) :
            (a : L.obj X ⟶ L.obj Y) → X ⟶ R.obj (L.obj Y))
          f ≫
        section_ (h.unit.app Y)) =
    f
have h₁ : L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
Tactic: suffices L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y) by simp [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
have h₁ : L.map (section_ (h.unit.app Y)) ≫ 𝟙 (L.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y)) = h.counit.app (L.obj Y)
Tactic: rw [← comp_id (L.map (section_ (h.unit.app Y)))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ f = g
have a : h.counit.app X ≫ f = h.counit.app X ≫ g
Tactic: apply Epi.left_cancellation (f := h.counit.app X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ h.counit.app X ≫ f = h.counit.app X ≫ g
have a : Eq.{v₁ + 1} (α := R.obj X ⟶ R.obj Y)
  (((h.homEquiv (R.obj X) Y : Equiv.{v₂ + 1, v₁ + 1} (L.obj (R.obj X) ⟶ Y) (R.obj X ⟶ R.obj Y)) :
        (a : L.obj (R.obj X) ⟶ Y) → R.obj X ⟶ R.obj Y)
      (h.counit.app X ≫ f) :
    R.obj X ⟶ R.obj Y)
  (((h.homEquiv (R.obj X) Y : Equiv.{v₂ + 1, v₁ + 1} (L.obj (R.obj X) ⟶ Y) (R.obj X ⟶ R.obj Y)) :
        (a : L.obj (R.obj X) ⟶ Y) → R.obj X ⟶ R.obj Y)
      (h.counit.app X ≫ g) :
    R.obj X ⟶ R.obj Y)
Tactic: apply (h.homEquiv (R.obj X) Y).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ ∃ (a : X ⟶ Y), R.map a = f
have h₁ : R.map
    (retraction (h.counit.app X) ≫
      ((Equiv.symm (h.homEquiv (R.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (R.obj X ⟶ R.obj Y) (L.obj (R.obj X) ⟶ Y)) :
          (a : R.obj X ⟶ R.obj Y) → L.obj (R.obj X) ⟶ Y)
        f) =
  f
Tactic: use (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map
      (retraction (h.counit.app X) ≫
        ((Equiv.symm (h.homEquiv (R.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (R.obj X ⟶ R.obj Y) (L.obj (R.obj X) ⟶ Y)) :
            (a : R.obj X ⟶ R.obj Y) → L.obj (R.obj X) ⟶ Y)
          f) =
    f
have h₁ : R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
Tactic: suffices R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X) by simp [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
have h₁ : 𝟙 (R.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)) ≫ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
Tactic: rw [← id_comp (R.map (retraction (h.counit.app X)))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
⊢ IsIso (L.whiskerLeft h.counit)
have this : whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)
Tactic: have := h.left_triangle
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (L.whiskerLeft h.counit)
have this₁ : L.whiskerLeft h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
Tactic: rw [← IsIso.eq_inv_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : L.whiskerLeft h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (L.whiskerLeft h.counit)
have rw : IsIso (inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
⊢ IsIso (whiskerRight h.counit R)
have this : R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
Tactic: have := h.right_triangle
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerRight h.counit R)
have this₁ : whiskerRight h.counit R = inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
Tactic: rw [← IsIso.eq_inv_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : whiskerRight h.counit R = inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerRight h.counit R)
have rw : IsIso (inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
⊢ IsIso (R.whiskerLeft h.unit)
have this : R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
Tactic: have := h.right_triangle
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (R.whiskerLeft h.unit)
have this₁ : R.whiskerLeft h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
Tactic: rw [← IsIso.eq_comp_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : R.whiskerLeft h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
⊢ IsIso (R.whiskerLeft h.unit)
have rw : IsIso (𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
⊢ IsIso (whiskerRight h.unit L)
have this : whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)
Tactic: have := h.left_triangle
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (whiskerRight h.unit L)
have this₁ : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit)
Tactic: rw [← IsIso.eq_comp_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit)
⊢ IsIso (whiskerRight h.unit L)
have rw : IsIso (𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
inst_3 : L.Full
X : D
⊢ IsIso (h.counit.app X) ↔ L.essImage X
have mp : IsIso (h.counit.app X) → L.essImage X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
inst_3 : L.Full
X : D
mp : IsIso (h.counit.app X) → L.essImage X
⊢ IsIso (h.counit.app X) ↔ L.essImage X
have mpr : L.essImage X → IsIso (h.counit.app X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
inst_3 : L.Full
X : D
w : C
i : L.obj w ≅ X
⊢ IsIso (h.counit.app X)
have mpr : IsIso (X := (R ⋙ L).obj (L.obj w)) (h.counit.app (L.obj w))
Tactic: rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Faithful
inst_3 : R.Full
Y : C
⊢ IsIso (h.unit.app Y) ↔ R.essImage Y
have mp : IsIso (h.unit.app Y) → R.essImage Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Faithful
inst_3 : R.Full
Y : C
mp : IsIso (h.unit.app Y) → R.essImage Y
⊢ IsIso (h.unit.app Y) ↔ R.essImage Y
have mpr : R.essImage Y → IsIso (h.unit.app Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Faithful
inst_3 : R.Full
Y : C
w : D
i : R.obj w ≅ Y
⊢ IsIso (h.unit.app Y)
have mpr : IsIso (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (R.obj w)) (h.unit.app (R.obj w))
Tactic: rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.IsEquivalence
⊢ IsIso h.unit
have this : ∀ (Y : C), IsIso (h.unit.app Y)
Tactic: have := fun Y => isIso_unit_app_of_iso h (R.objObjPreimageIso Y).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.IsEquivalence
⊢ IsIso h.counit
have this : ∀ (X : D), IsIso (h.counit.app X)
Tactic: have := fun X => isIso_counit_app_of_iso h (L.objObjPreimageIso X).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.IsEquivalence
⊢ IsIso h.unit
have this : R.IsEquivalence
Tactic: have := h.isEquivalence_right_of_isEquivalence_left
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.IsEquivalence
⊢ IsIso h.counit
have this : L.IsEquivalence
Tactic: have := h.isEquivalence_left_of_isEquivalence_right
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
⊢ IsIso (T.map (h.unit.app X))
have hf : ∀ (T_1 : E),
  Function.Bijective (β := T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ T_1) fun (x : T.obj ((L ⋙ R).obj X) ⟶ T_1) ↦
    T.map (h.unit.app X) ≫ x
Tactic: apply isIso_of_coyoneda_map_bijective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
⊢ Function.Bijective (β := T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) fun (x : T.obj ((L ⋙ R).obj X) ⟶ Y) ↦
    T.map (h.unit.app X) ≫ x
have h₁ : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y) →
  (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) = (T.obj X ⟶ Y) →
    Eq (α := (T.obj ((L ⋙ R).obj X) ⟶ Y) → (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y))
      (fun (x : T.obj ((L ⋙ R).obj X) ⟶ Y) ↦ T.map (h.unit.app X) ≫ x)
      (⇑(Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
            (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm))) :
        (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)
Tactic: convert!
    ((adj2.homEquiv (R.obj (L.obj X)) Y).trans <|
        FF.homEquiv.symm.trans <|
          (h.homEquiv X (S.obj Y)).trans (adj2.homEquiv X Y).symm).bijective using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1 : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2 : (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) = (T.obj X ⟶ Y)
⊢ Eq (α := (T.obj ((L ⋙ R).obj X) ⟶ Y) → (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y))
    (fun (x : T.obj ((L ⋙ R).obj X) ⟶ Y) ↦ T.map (h.unit.app X) ≫ x)
    (⇑(Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
          (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm))) :
      (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)
have h₁ : ∀ (x : T.obj ((L ⋙ R).obj X) ⟶ Y),
  T.map (h.unit.app X) ≫ x =
    (Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
          (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm)) :
        (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1 : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2 : (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) = (T.obj X ⟶ Y)
x : T.obj ((L ⋙ R).obj X) ⟶ Y
⊢ T.map (h.unit.app X) ≫ x =
    (Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
          (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm)) :
        (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)
      x
have this : T.map ((S ⋙ R).map x) ≫ adj2.counit.app Y = adj2.counit.app (T.obj ((L ⋙ R).obj X)) ≫ x
Tactic: have := adj2.counit_naturality x
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Left (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ F'.map (U.map (adj₁.counit.app X)) =
    𝟙 (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))
have rw : F'.map (𝟙 (U.obj X)) = 𝟙 (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))
Tactic: rw [← F'.map_comp, adj₁.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Left (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ otherMap R F' adj₁ adj₂ X =
    𝟙 (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))
have dsimp : F'.map (adj₁.unit.app (U.obj X)) ≫
    F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
  𝟙 (F'.obj (U.obj X))
Tactic: dsimp [otherMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Left (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫
      F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
        adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
have rw : F'.map (adj₁.unit.app (U.obj X) ≫ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
    adj₂.counit.app (F'.obj (U.1 X)) =
  𝟙 (F'.obj (U.obj X))
Tactic: rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc,
        adj₁.right_triangle_components, comp_id, adj₂.left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Left (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
rw :
  F'.map (adj₁.unit.app (U.obj X) ≫ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫
      F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
        adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
have rw₁ : F'.map
      (adj₁.unit.app (U.obj X) ≫
        U.map (F.map (adj₂.unit.app (U.1 X))) ≫ U.map (adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
    adj₂.counit.app (F'.obj (U.1 X)) =
  𝟙 (F'.obj (U.obj X))
Tactic: rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc,
        adj₁.right_triangle_components, comp_id, adj₂.left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Left (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
rw :
  F'.map (adj₁.unit.app (U.obj X) ≫ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
rw₁ :
  F'.map
        (adj₁.unit.app (U.obj X) ≫
          U.map (F.map (adj₂.unit.app (U.1 X))) ≫ U.map (adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫
      F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
        adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
have rw₂ : F'.map
      (adj₂.unit.app (U.1 X) ≫
        adj₁.unit.app (U.obj (R.obj (F'.obj (U.1 X)))) ≫ U.map (adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
    adj₂.counit.app (F'.obj (U.1 X)) =
  𝟙 (F'.obj (U.obj X))
Tactic: rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc,
        adj₁.right_triangle_components, comp_id, adj₂.left_triangle_components]