awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.adj₁.counit.app (H.obj X) ≫ t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X))
⊢ Epi (t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X))
have rw₁ : Epi (F.map (t.adj₂.counit.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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Triple (hypothesis)
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
inst_4 : H.PreservesEpimorphisms
X : C
⊢ Epi (t.rightToLeft.app X) ↔ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)
have x : G.IsLeftAdjoint
Tactic: have _ := t.adj₂.isLeftAdjoint
-- 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
inst_4 : H.PreservesEpimorphisms
X : C
h_1 : G.IsLeftAdjoint
h : Epi (t.rightToLeft.app X)
⊢ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)
have rw : Epi (G.map (t.rightToLeft.app X))
Tactic: rw [← map_rightToLeft_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
inst_4 : H.PreservesEpimorphisms
X : C
h : G.IsLeftAdjoint
⊢ Epi (t.rightToLeft.app X) ↔ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)
have refine : ∀ (h : Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)), Epi (t.rightToLeft.app X)
Tactic: refine ⟨fun h ↦ by rw [← map_rightToLeft_app]; exact G.map_epi _, fun h ↦ ?_⟩
-- 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
inst_4 : H.PreservesEpimorphisms
X : C
h_1 : G.IsLeftAdjoint
h : Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)
⊢ Epi (t.rightToLeft.app X)
have rw : Epi (H.map (t.adj₁.unit.app X))
Tactic: rw [epi_rightToLeft_app_iff_epi_map_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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
⊢ t.leftToRight =
    F.leftUnitor.inv ≫
      inv (whiskerRight t.adj₂.counit F) ≫ (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom
have w : ∀ (X : C),
  t.leftToRight.app X =
    (F.leftUnitor.inv ≫
          inv (whiskerRight t.adj₂.counit F) ≫
            (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ t.leftToRight.app X =
    (F.leftUnitor.inv ≫
          inv (whiskerRight t.adj₂.counit F) ≫
            (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom).app
      X
have w : 𝟙 (F.obj X) ≫
    t.adj₂.unit.app (F.obj X) ≫ 𝟙 (H.obj (G.obj (F.obj X))) ≫ (inv (whiskerRight t.adj₁.unit H)).app X ≫ 𝟙 (H.obj X) =
  𝟙 (F.obj X) ≫
    (inv (whiskerRight t.adj₂.counit F)).app X ≫ 𝟙 (F.obj (G.obj (H.obj X))) ≫ t.adj₁.counit.app (H.obj X) ≫ 𝟙 (H.obj X)
Tactic: dsimp [leftToRight]
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ 𝟙 (F.obj X) ≫
      t.adj₂.unit.app (F.obj X) ≫ 𝟙 (H.obj (G.obj (F.obj X))) ≫ (inv (whiskerRight t.adj₁.unit H)).app X ≫ 𝟙 (H.obj X) =
    𝟙 (F.obj X) ≫
      (inv (whiskerRight t.adj₂.counit F)).app X ≫
        𝟙 (F.obj (G.obj (H.obj X))) ≫ t.adj₁.counit.app (H.obj X) ≫ 𝟙 (H.obj X)
have w : t.adj₂.unit.app (F.obj X) ≫ inv ((whiskerRight t.adj₁.unit H).app X) =
  inv ((whiskerRight t.adj₂.counit F).app X) ≫ t.adj₁.counit.app (H.obj X)
Tactic: simp only [Category.id_comp, Category.comp_id, NatIso.isIso_inv_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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ t.adj₂.unit.app (F.obj X) ≫ inv ((whiskerRight t.adj₁.unit H).app X) =
    inv ((whiskerRight t.adj₂.counit F).app X) ≫ t.adj₁.counit.app (H.obj X)
have w : (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
  t.adj₁.counit.app (H.obj X) ≫ (whiskerRight t.adj₁.unit H).app X
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, IsIso.eq_inv_comp]
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    t.adj₁.counit.app (H.obj X) ≫ (whiskerRight t.adj₁.unit H).app X
have w : (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
  F.map (G.map ((whiskerRight t.adj₁.unit H).app X)) ≫ t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
Tactic: refine Eq.trans ?_ (t.adj₁.counit_naturality <| (whiskerRight t.adj₁.unit H).app 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map (G.map ((whiskerRight t.adj₁.unit H).app X)) ≫ t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
have w : (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
  F.map
      ((t.adj₂.counit.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ≫ t.adj₁.unit.app X) ≫ G.map (t.adj₂.unit.app (F.obj X))) ≫
    t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
Tactic: rw [whiskerRight_app _ H, (asIso (t.adj₂.counit.app (G.obj _))).eq_comp_inv.2
      (t.adj₂.counit_naturality (t.adj₁.unit.app X)),
    ← (asIso _).comp_hom_eq_id.1 <| t.adj₂.left_triangle_components (F.obj 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 : F.Full
inst_3 : F.Faithful
X : D
⊢ t.leftToRight.app (G.obj X) = t.adj₁.counit.app X ≫ t.adj₂.unit.app X
have refine : Eq.{v_2 + 1} (α := F.obj (G.obj X) ⟶ H.obj (G.obj X))
  (((t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X) :
          Equiv.{v_1 + 1, v_2 + 1} (G.obj (F.obj (G.obj X)) ⟶ G.obj X) (F.obj (G.obj X) ⟶ H.obj (G.obj X))) :
        (a : G.obj (F.obj (G.obj X)) ⟶ G.obj X) → F.obj (G.obj X) ⟶ H.obj (G.obj X))
      (((Equiv.symm (t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X)) :
            Equiv.{v_2 + 1, v_1 + 1} (F.obj (G.obj X) ⟶ H.obj (G.obj X)) (G.obj (F.obj (G.obj X)) ⟶ G.obj X)) :
          (a : F.obj (G.obj X) ⟶ H.obj (G.obj X)) → G.obj (F.obj (G.obj X)) ⟶ G.obj X)
        (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)) :
    F.obj (G.obj X) ⟶ H.obj (G.obj X))
  (t.leftToRight.app (G.obj X) : F.obj (G.obj X) ⟶ H.obj (G.obj X))
Tactic: refine (((t.adj₂.homEquiv _ _).apply_symm_apply _).symm.trans ?_).symm
-- 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 : F.Full
inst_3 : F.Faithful
X : D
⊢ Eq.{v_2 + 1} (α := F.obj (G.obj X) ⟶ H.obj (G.obj X))
    (((t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X) :
            Equiv.{v_1 + 1, v_2 + 1} (G.obj (F.obj (G.obj X)) ⟶ G.obj X) (F.obj (G.obj X) ⟶ H.obj (G.obj X))) :
          (a : G.obj (F.obj (G.obj X)) ⟶ G.obj X) → F.obj (G.obj X) ⟶ H.obj (G.obj X))
        (((Equiv.symm (t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X)) :
              Equiv.{v_2 + 1, v_1 + 1} (F.obj (G.obj X) ⟶ H.obj (G.obj X)) (G.obj (F.obj (G.obj X)) ⟶ G.obj X)) :
            (a : F.obj (G.obj X) ⟶ H.obj (G.obj X)) → G.obj (F.obj (G.obj X)) ⟶ G.obj X)
          (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)) :
      F.obj (G.obj X) ⟶ H.obj (G.obj X))
    (t.leftToRight.app (G.obj X) : F.obj (G.obj X) ⟶ H.obj (G.obj X))
have rw : t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
  t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))
Tactic: rw [homEquiv_symm_apply, map_comp, Category.assoc, left_triangle_components,
    homEquiv_apply, leftToRight_app, ← H.map_inv]
-- 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 : F.Full
inst_3 : F.Faithful
X : D
⊢ t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))
have e_a : G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X) = inv (t.adj₁.unit.app (G.obj X))
Tactic: congr
-- 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 : F.Full
inst_3 : F.Faithful
⊢ G.whiskerLeft t.leftToRight = t.adj₁.counit ≫ t.adj₂.unit
have w : ∀ (X : D), (G.whiskerLeft t.leftToRight).app X = (t.adj₁.counit ≫ t.adj₂.unit).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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
⊢ t.op.leftToRight = NatTrans.op t.leftToRight
have w : ∀ (x : Cᵒᵖ), t.op.leftToRight.app x = (NatTrans.op t.leftToRight).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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
x : Cᵒᵖ
⊢ t.op.leftToRight.app x = (NatTrans.op t.leftToRight).app x
have w : (H.op.rightUnitor.inv ≫
        H.op.whiskerLeft t.op.adj₂.unit ≫
          (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
    x =
  (NatTrans.op
        (F.leftUnitor.inv ≫
          inv (whiskerRight t.adj₂.counit F) ≫
            (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom)).app
    x
Tactic: rw [leftToRight, leftToRight_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 : F.Full
inst_3 : F.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj X)) (t.adj₂.unit.app (F.obj X))
have rw : Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X ≫ H.map (t.adj₁.unit.app X))
Tactic: rw [← leftToRight_app_map_adj₁_unit_app, mono_comp_iff_of_mono]
-- 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 : F.Full
inst_3 : F.Faithful
X : C
rw : Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X ≫ H.map (t.adj₁.unit.app X))
⊢ Mono (t.leftToRight.app X) ↔ Mono (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj X)) (t.adj₂.unit.app (F.obj X))
have rw₁ : Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)
Tactic: rw [← leftToRight_app_map_adj₁_unit_app, mono_comp_iff_of_mono]
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (X := (G ⋙ F).obj (H.obj X)) (t.adj₁.counit.app (H.obj X))
have rw : Mono (t.leftToRight.app X) ↔ Mono (F.map (t.adj₂.counit.app X) ≫ t.leftToRight.app X)
Tactic: rw [← map_adj₂_counit_app_leftToRight_app, mono_comp_iff_of_isIso]
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
rw : Mono (t.leftToRight.app X) ↔ Mono (F.map (t.adj₂.counit.app X) ≫ t.leftToRight.app X)
⊢ Mono (t.leftToRight.app X) ↔ Mono (X := (G ⋙ F).obj (H.obj X)) (t.adj₁.counit.app (H.obj X))
have rw₁ : Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)
Tactic: rw [← map_adj₂_counit_app_leftToRight_app, mono_comp_iff_of_isIso]
-- 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 : F.Full
inst_3 : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
have rw : Mono (X := F.obj (G.obj X)) (t.leftToRight.app (G.obj X))
Tactic: rw [← leftToRight_app_obj]
-- 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 : F.Full
inst_3 : F.Faithful
⊢ (∀ (X : C), Mono (t.leftToRight.app X)) ↔ ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
have refine : ∀ (h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)) (X : C), Mono (t.leftToRight.app X)
Tactic: refine ⟨fun h X ↦ by rw [← leftToRight_app_obj]; exact h _, fun h 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 : F.Full
inst_3 : F.Faithful
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.leftToRight.app X)
have rw : Mono (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj X)) (t.adj₂.unit.app (F.obj X))
Tactic: rw [mono_leftToRight_app_iff_mono_adj₂_unit_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit
have w : ∀ (x : C), (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x
have w : adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x =
  ((adj1.homEquiv x (F'.obj x) : Equiv.{v_2 + 1, v_1 + 1} (F.obj x ⟶ F'.obj x) (x ⟶ G.obj (F'.obj x))) :
      (a : F.obj x ⟶ F'.obj x) → x ⟶ G.obj (F'.obj x))
    ((adj1.leftAdjointUniq adj2).hom.app x)
Tactic: rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x
have rw : adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
  (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x
Tactic: rw [← unit_leftAdjointUniq_hom adj1 adj2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit = adj1.counit
have w : ∀ (x : D), (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x
have w : F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x
Tactic: simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom,
    conjugateIsoEquiv_symm_apply_inv, Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app,
    conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp,
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x
have w : F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x
Tactic: rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x
have rw : (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x =
  (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x
Tactic: rw [← leftAdjointUniq_hom_counit adj1 adj2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 F' F'' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x
have rw : (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x =
  ((adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom).app x
Tactic: rw [← leftAdjointUniq_trans adj1 adj2 adj3]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ (adj1.rightAdjointUniq adj2).hom.app (F.obj x) = adj2.unit.app x
have simp : adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x
Tactic: simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, conjugateIsoEquiv_apply_hom,
    Iso.refl_hom, conjugateEquiv_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x
have rw : adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x) ≫ adj1.counit.app (F.obj x)) = adj2.unit.app x
Tactic: rw [← adj2.unit_naturality_assoc, ← G'.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom = adj2.unit
have w : ∀ (x : C), (adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom).app x = adj2.unit.app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (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 G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit = adj1.counit
have w : ∀ (x : D), (whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit).app x = adj1.counit.app x
Tactic: ext