awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
simp_rw :
  (∀ (X : C) (Z : D),
      Function.Injective (β := L.obj (F.obj (G.obj X)) ⟶ Z) fun (g : L.obj X ⟶ Z) ↦ L.map (q.adj₂.counit.app X) ≫ g) ↔
    ∀ (X : D) (Z : C),
      Function.Injective (β := Z ⟶ R.obj (G.obj (F.obj X))) fun (g : Z ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)
⊢ (∀ (X : C), Epi (inv (q.adj₁.counit.app (G.obj X)) ≫ L.map (q.adj₂.counit.app X))) ↔
    ∀ (X : D), Mono (X := F.obj X) (q.adj₃.unit.app (F.obj X))

Tactic:
simp_rw [epi_comp_iff_of_epi, epi_iff_forall_injective, mono_iff_forall_injective]

Premises used: CategoryTheory.epi_comp_iff_of_epi, CategoryTheory.epi_iff_forall_injective, CategoryTheory.mono_iff_forall_injective
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
rw :
  (∀ (b : D) (a : C),
      Function.Injective (β := L.obj (F.obj (G.obj a)) ⟶ b) fun (g : L.obj a ⟶ b) ↦ L.map (q.adj₂.counit.app a) ≫ g) ↔
    ∀ (X : D) (Z : C),
      Function.Injective (β := Z ⟶ R.obj (G.obj (F.obj X))) fun (g : Z ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)
⊢ (∀ (X : C) (Z : D),
      Function.Injective (β := L.obj (F.obj (G.obj X)) ⟶ Z) fun (g : L.obj X ⟶ Z) ↦ L.map (q.adj₂.counit.app X) ≫ g) ↔
    ∀ (X : D) (Z : C),
      Function.Injective (β := Z ⟶ R.obj (G.obj (F.obj X))) fun (g : Z ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
rw [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
⊢ (∀ (b : D) (a : C),
      Function.Injective (β := L.obj (F.obj (G.obj a)) ⟶ b) fun (g : L.obj a ⟶ b) ↦ L.map (q.adj₂.counit.app a) ≫ g) ↔
    ∀ (X : D) (Z : C),
      Function.Injective (β := Z ⟶ R.obj (G.obj (F.obj X))) fun (g : Z ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
forall_congr' fun X ↦ forall_congr' fun Y ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
refine :
  ∀ (X : D) (Y : C),
    (Function.Injective (β := L.obj (F.obj (G.obj Y)) ⟶ X) fun (g : L.obj Y ⟶ X) ↦ L.map (q.adj₂.counit.app Y) ≫ g) ↔
      Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)
⊢ (∀ (b : D) (a : C),
      Function.Injective (β := L.obj (F.obj (G.obj a)) ⟶ b) fun (g : L.obj a ⟶ b) ↦ L.map (q.adj₂.counit.app a) ≫ g) ↔
    ∀ (X : D) (Z : C),
      Function.Injective (β := Z ⟶ R.obj (G.obj (F.obj X))) fun (g : Z ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
refine forall_congr' fun X ↦ forall_congr' fun Y ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
rw :
  Function.Injective.{v₂ + 1, v₁ + 1} (α := L.obj Y ⟶ X) (β := F.obj (G.obj Y) ⟶ F.obj X)
      (Function.comp (β := L.obj (F.obj (G.obj Y)) ⟶ X)
        (⇑(q.adj₁.homEquiv (F.obj (G.obj Y)) X) : (a : L.obj (F.obj (G.obj Y)) ⟶ X) → F.obj (G.obj Y) ⟶ F.obj X)
        fun (g : L.obj Y ⟶ X) ↦ L.map (q.adj₂.counit.app Y) ≫ g) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)
⊢ (Function.Injective (β := L.obj (F.obj (G.obj Y)) ⟶ X) fun (g : L.obj Y ⟶ X) ↦ L.map (q.adj₂.counit.app Y) ≫ g) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
rw [← (q.adj₁.homEquiv _ _).comp_injective _]

Premises used: CategoryTheory.Adjunction.Quadruple.adj₁, CategoryTheory.Adjunction.homEquiv, Equiv.comp_injective
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
simp_rw :
  (Function.Injective.{v₂ + 1, v₁ + 1} (β := F.obj (G.obj Y) ⟶ F.obj X) fun (x : L.obj Y ⟶ X) ↦
      q.adj₂.counit.app Y ≫ (q.adj₁.homEquiv Y X : (a : L.obj Y ⟶ X) → Y ⟶ F.obj X) x) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)
⊢ Function.Injective.{v₂ + 1, v₁ + 1} (α := L.obj Y ⟶ X) (β := F.obj (G.obj Y) ⟶ F.obj X)
      (Function.comp (β := L.obj (F.obj (G.obj Y)) ⟶ X)
        (⇑(q.adj₁.homEquiv (F.obj (G.obj Y)) X) : (a : L.obj (F.obj (G.obj Y)) ⟶ X) → F.obj (G.obj Y) ⟶ F.obj X)
        fun (g : L.obj Y ⟶ X) ↦ L.map (q.adj₂.counit.app Y) ≫ g) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
simp_rw [Function.comp_def, q.adj₁.homEquiv_naturality_left]

Premises used: CategoryTheory.Adjunction.Quadruple.adj₁, Function.comp_def, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
⊢ (Function.Injective.{v₂ + 1, v₁ + 1} (β := F.obj (G.obj Y) ⟶ F.obj X) fun (x : L.obj Y ⟶ X) ↦
      q.adj₂.counit.app Y ≫ (q.adj₁.homEquiv Y X : (a : L.obj Y ⟶ X) → Y ⟶ F.obj X) x) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
((q.adj₁.homEquiv _ _).injective_comp fun f ↦ _).trans ?_

Premises used: CategoryTheory.Adjunction.Quadruple.adj₁, Equiv.injective_comp, Iff.trans, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
rw :
  Function.Injective (α := Y ⟶ F.obj X) (β := Y ⟶ R.obj (G.obj (F.obj X)))
      (Function.comp (β := F.obj (G.obj Y) ⟶ F.obj X)
        (⇑(Equiv.trans (q.adj₂.homEquiv (G.obj Y) (F.obj X)) (q.adj₃.homEquiv Y (G.obj (F.obj X)))) :
          (a : F.obj (G.obj Y) ⟶ F.obj X) → Y ⟶ R.obj (G.obj (F.obj X)))
        fun (f : Y ⟶ F.obj X) ↦ q.adj₂.counit.app Y ≫ f) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)
⊢ (Function.Injective (β := F.obj (G.obj Y) ⟶ F.obj X) fun (f : Y ⟶ F.obj X) ↦ q.adj₂.counit.app Y ≫ f) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
rw [← ((q.adj₂.homEquiv _ _).trans (q.adj₃.homEquiv _ _)).comp_injective _]

Premises used: CategoryTheory.Adjunction.Quadruple.adj₃, CategoryTheory.Adjunction.Quadruple.adj₂, Equiv.trans, CategoryTheory.Adjunction.homEquiv, Equiv.comp_injective
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
X : D
Y : C
⊢ Function.Injective (α := Y ⟶ F.obj X) (β := Y ⟶ R.obj (G.obj (F.obj X)))
      (Function.comp (β := F.obj (G.obj Y) ⟶ F.obj X)
        (⇑(Equiv.trans (q.adj₂.homEquiv (G.obj Y) (F.obj X)) (q.adj₃.homEquiv Y (G.obj (F.obj X)))) :
          (a : F.obj (G.obj Y) ⟶ F.obj X) → Y ⟶ R.obj (G.obj (F.obj X)))
        fun (f : Y ⟶ F.obj X) ↦ q.adj₂.counit.app Y ≫ f) ↔
    Function.Injective (β := Y ⟶ R.obj (G.obj (F.obj X))) fun (g : Y ⟶ F.obj X) ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
simp [Function.comp_def, ← q.adj₂.homEquiv_symm_id, ← q.adj₂.homEquiv_naturality_right_symm,
    ← q.adj₃.homEquiv_id, ← q.adj₃.homEquiv_naturality_left]

Premises used: CategoryTheory.Adjunction.Quadruple.adj₃, CategoryTheory.Adjunction.Quadruple.adj₂, Function.comp_def, CategoryTheory.Adjunction.homEquiv_symm_id, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_id, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : HasPushouts.{v₂, u₂} D
rw : (∀ (k : C), Epi (q.leftTriple.rightToLeft.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.leftToRight.app k)
⊢ Epi q.leftTriple.rightToLeft ↔ Mono q.rightTriple.leftToRight

Tactic:
rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]

Premises used: CategoryTheory.NatTrans.epi_iff_epi_app, CategoryTheory.NatTrans.mono_iff_mono_app
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : HasPushouts.{v₂, u₂} D
⊢ (∀ (k : C), Epi (q.leftTriple.rightToLeft.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.leftToRight.app k)

Tactic:
q.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app

Premises used: CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : HasPushouts.{v₂, u₂} D
⊢ (∀ (k : C), Epi (q.leftTriple.rightToLeft.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.leftToRight.app k)

Tactic:
exact q.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app

Premises used: CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : L.Full
inst_3 : L.Faithful
inst_4 : G.Full
inst_5 : G.Faithful
⊢ (∀ (X : Dᵒᵖ), Epi (q.op.leftTriple.rightToLeft.app X)) ↔ ∀ (X : Cᵒᵖ), Mono (q.op.rightTriple.leftToRight.app X)

Tactic:
have h := q.op.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : L.Full
inst_3 : L.Faithful
inst_4 : G.Full
inst_5 : G.Faithful
h : (∀ (X : Dᵒᵖ), Epi (q.op.leftTriple.rightToLeft.app X)) ↔ ∀ (X : Cᵒᵖ), Mono (q.op.rightTriple.leftToRight.app X)
⊢ (∀ (X : Dᵒᵖ), Epi (q.op.leftTriple.rightToLeft.app X)) ↔
    ∀ (a : C),
      Mono (X := G.op.obj ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))
        (q.op.rightTriple.leftToRight.app ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))

Tactic:
rw [← (Opposite.equivToOpposite (α := C)).forall_congr_right] at h

Premises used: Opposite.equivToOpposite, Equiv.forall_congr_right
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : L.Full
inst_3 : L.Faithful
inst_4 : G.Full
inst_5 : G.Faithful
h :
  (∀ (X : Dᵒᵖ), Epi (q.op.leftTriple.rightToLeft.app X)) ↔
    ∀ (a : C),
      Mono (X := G.op.obj ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))
        (q.op.rightTriple.leftToRight.app ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))
⊢ (∀ (a : D),
      Epi (X := F.op.obj ((Opposite.equivToOpposite : (a : D) → Dᵒᵖ) a))
        (q.op.leftTriple.rightToLeft.app ((Opposite.equivToOpposite : (a : D) → Dᵒᵖ) a))) ↔
    ∀ (a : C),
      Mono (X := G.op.obj ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))
        (q.op.rightTriple.leftToRight.app ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))

Tactic:
rw [← (Opposite.equivToOpposite (α := D)).forall_congr_right] at h

Premises used: Opposite.equivToOpposite, Equiv.forall_congr_right
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : L.Full
inst_3 : L.Faithful
inst_4 : G.Full
inst_5 : G.Faithful
h :
  (∀ (a : D),
      Epi (X := F.op.obj ((Opposite.equivToOpposite : (a : D) → Dᵒᵖ) a))
        (q.op.leftTriple.rightToLeft.app ((Opposite.equivToOpposite : (a : D) → Dᵒᵖ) a))) ↔
    ∀ (a : C),
      Mono (X := G.op.obj ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))
        (q.op.rightTriple.leftToRight.app ((Opposite.equivToOpposite : (a : C) → Cᵒᵖ) a))
⊢ (∀ (X : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)

Tactic:
simpa using h.symm

Premises used: Iff.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : L.Full
inst_3 : L.Faithful
inst_4 : G.Full
inst_5 : G.Faithful
inst_6 : HasPullbacks.{v₁, u₁} C
inst_7 : HasPushouts.{v₂, u₂} D
rw : (∀ (k : C), Epi (q.leftTriple.leftToRight.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.rightToLeft.app k)
⊢ Epi q.leftTriple.leftToRight ↔ Mono q.rightTriple.rightToLeft

Tactic:
rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]

Premises used: CategoryTheory.NatTrans.epi_iff_epi_app, CategoryTheory.NatTrans.mono_iff_mono_app
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : L.Full
inst_3 : L.Faithful
inst_4 : G.Full
inst_5 : G.Faithful
inst_6 : HasPullbacks.{v₁, u₁} C
inst_7 : HasPushouts.{v₂, u₂} D
⊢ (∀ (k : C), Epi (q.leftTriple.leftToRight.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.rightToLeft.app k)

Tactic:
q.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app

Premises used: CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : L.Full
inst_3 : L.Faithful
inst_4 : G.Full
inst_5 : G.Faithful
inst_6 : HasPullbacks.{v₁, u₁} C
inst_7 : HasPushouts.{v₂, u₂} D
⊢ (∀ (k : C), Epi (q.leftTriple.leftToRight.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.rightToLeft.app k)

Tactic:
exact q.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app

Premises used: CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app
-- 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
⊢ i.IsRightAdjoint

Tactic:
⟨_, ⟨reflectorAdjunction i⟩⟩

Premises used: Nonempty.intro, CategoryTheory.reflectorAdjunction, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.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
inst_3 : Reflective i
⊢ (reflector i).IsLeftAdjoint

Tactic:
⟨_, ⟨reflectorAdjunction i⟩⟩

Premises used: Nonempty.intro, CategoryTheory.reflectorAdjunction, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- 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
X : C
rw :
  CategoryStruct.comp (Y := i.obj ((i ⋙ reflector i).obj ((reflector i).obj X)))
      (NatTrans.app (unit (reflectorAdjunction i)) (i.obj ((reflector i).obj X)))
      (i.map (NatTrans.app (counit (reflectorAdjunction i)) ((reflector i).obj X))) =
    i.map
      ((reflector i).map (NatTrans.app (unit (reflectorAdjunction i)) X) ≫
        NatTrans.app (counit (reflectorAdjunction i)) ((reflector i).obj X))
⊢ NatTrans.app (unit (reflectorAdjunction i)) (i.obj ((reflector i).obj X)) =
    i.map ((reflector i).map (NatTrans.app (unit (reflectorAdjunction i)) X))

Tactic:
rw [← cancel_mono (i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X))),
    ← i.map_comp]

Premises used: CategoryTheory.reflector, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.reflectorAdjunction, CategoryTheory.Functor.map_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
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
X : C
⊢ CategoryStruct.comp (Y := i.obj ((i ⋙ reflector i).obj ((reflector i).obj X)))
      (NatTrans.app (unit (reflectorAdjunction i)) (i.obj ((reflector i).obj X)))
      (i.map (NatTrans.app (counit (reflectorAdjunction i)) ((reflector i).obj X))) =
    i.map
      ((reflector i).map (NatTrans.app (unit (reflectorAdjunction i)) X) ≫
        NatTrans.app (counit (reflectorAdjunction i)) ((reflector i).obj 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
inst_3 : Reflective i
B : D
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (i.obj B)) (Y := (reflector i ⋙ i).obj (i.obj B))
    (NatTrans.app (unit (reflectorAdjunction i)) (i.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
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A : C
h rwa rwa₁ rwa₂ rwa₃ : i.essImage A
⊢ IsIso (Y := (reflector i ⋙ i).obj A) (NatTrans.app (unit (reflectorAdjunction i)) A)

Tactic:
rwa [isIso_unit_app_iff_mem_essImage]

Premises used: CategoryTheory.Adjunction.isIso_unit_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
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)
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (i.obj ((reflector i).obj A))) (η.app (i.obj ((reflector i).obj A)))

Tactic:
haveI : IsIso (η.app (i.obj ((reflector i).obj A))) :=
    Functor.essImage.unit_isIso ((i.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
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:
@epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.app A) ?_

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.retraction, 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
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)))
refine : Epi (retraction (η.app A) ≫ η.app A)
⊢ Epi (η.app A)

Tactic:
refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.app A) ?_

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.retraction, 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
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)))
rw : Epi (η.app ((reflector i ⋙ i).obj A) ≫ (reflector i ⋙ i).map (retraction (η.app A)))
⊢ Epi (retraction (η.app A) ≫ η.app A)

Tactic:
rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]

Premises used: CategoryTheory.retraction, CategoryTheory.NatTrans.naturality, 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
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 ((reflector i ⋙ i).obj A) ≫ (reflector i ⋙ i).map (retraction (η.app A)))

Tactic:
apply epi_comp (η.app (i.obj ((reflector i).obj A)))

Premises used: CategoryTheory.epi_comp, CategoryTheory.reflector, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app