awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ obj yoneda c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
⊢ Eq.{v₂ + 1} (α :=
    F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : ((const J).obj Y).obj j ⟶ F.partialRightAdjointObj (R.obj j')) →
            F.obj (((const J).obj Y).obj j) ⟶ (R.obj j').obj)
        (map (obj (const J) Y) φ ≫
          ((Equiv.symm F.partialRightAdjointHomEquiv :
                Equiv.{v₂ + 1, v₁ + 1}
                  (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j') ⟶
                    (R.obj j').obj (P := F.rightAdjointObjIsDefined))
                  (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j' ⟶ F.partialRightAdjointObj (R.obj j'))) :
              (a : F.obj (((const J).obj Y).obj j') ⟶ (R.obj j').obj) →
                ((const J).obj Y).obj j' ⟶ F.partialRightAdjointObj (R.obj j'))
            (g ≫ c.π.app j')) :
      F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : ((const J).obj Y).obj j ⟶ F.partialRightAdjointObj (R.obj j')) →
            F.obj (((const J).obj Y).obj j) ⟶ (R.obj j').obj)
        (((Equiv.symm F.partialRightAdjointHomEquiv :
                Equiv.{v₂ + 1, v₁ + 1}
                  (F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))
                  (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j ⟶ F.partialRightAdjointObj (R.obj j))) :
              (a : F.obj (((const J).obj Y).obj j) ⟶ (R.obj j).obj) →
                ((const J).obj Y).obj j ⟶ F.partialRightAdjointObj (R.obj j))
            (g ≫ c.π.app j) ≫
          (R ⋙ F.partialRightAdjoint).map φ) :
      F.obj (obj.{v_1, v₁, u_1, u₁} (obj (const J) Y) j) ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
have this : c.π.app j ≫ (R ⋙ F.rightAdjointObjIsDefined.ι).map φ = c.π.app j'
Tactic: have := c.w φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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 : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.leftToRight.app X)
have simp_rw : (∀ (X : C),
    Epi
      ((G.rightUnitor.inv ≫
            inv (G.whiskerLeft q.leftTriple.adj₁.counit) ≫
              (G.associator F L).inv ≫ whiskerRight q.leftTriple.adj₂.counit L ≫ L.leftUnitor.hom).app
        X)) ↔
  ∀ (X : D), Mono (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (F.obj X)) (q.rightTriple.adj₂.unit.app (F.obj X))
Tactic: simp_rw [mono_leftToRight_app_iff_mono_adj₂_unit_app, rightToLeft_eq_counits]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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 : C),
      Epi
        ((G.rightUnitor.inv ≫
              inv (G.whiskerLeft q.leftTriple.adj₁.counit) ≫
                (G.associator F L).inv ≫ whiskerRight q.leftTriple.adj₂.counit L ≫ L.leftUnitor.hom).app
          X)) ↔
    ∀ (X : D), Mono (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (F.obj X)) (q.rightTriple.adj₂.unit.app (F.obj X))
have dsimp : (∀ (X : C),
    Epi
      (𝟙 (G.obj X) ≫
        (inv (G.whiskerLeft q.adj₁.counit)).app X ≫
          𝟙 (L.obj (F.obj (G.obj X))) ≫ L.map (q.adj₂.counit.app X) ≫ 𝟙 (L.obj X))) ↔
  ∀ (X : D), Mono (X := F.obj X) (q.adj₃.unit.app (F.obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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 : C),
      Epi
        (𝟙 (G.obj X) ≫
          (inv (G.whiskerLeft q.adj₁.counit)).app X ≫
            𝟙 (L.obj (F.obj (G.obj X))) ≫ L.map (q.adj₂.counit.app X) ≫ 𝟙 (L.obj X))) ↔
    ∀ (X : D), Mono (X := F.obj X) (q.adj₃.unit.app (F.obj X))
have simp : (∀ (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 only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.id_obj,
    whiskerLeft_app, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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 : 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))
have 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)
Tactic: simp_rw [epi_comp_iff_of_epi, epi_iff_forall_injective, mono_iff_forall_injective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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 : 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)
have 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)
Tactic: rw [forall_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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)
have 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)
Tactic: refine forall_congr' fun X ↦ forall_congr' fun Y ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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 (β := 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)
have 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)
Tactic: rw [← (q.adj₁.homEquiv _ _).comp_injective _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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} (α := 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)
have 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)
Tactic: simp_rw [Function.comp_def, q.adj₁.homEquiv_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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 (β := 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)
have 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)
Tactic: rw [← ((q.adj₂.homEquiv _ _).trans (q.adj₃.homEquiv _ _)).comp_injective _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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
⊢ Epi q.leftTriple.rightToLeft ↔ Mono q.rightTriple.leftToRight
have rw : (∀ (k : C), Epi (q.leftTriple.rightToLeft.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.leftToRight.app k)
Tactic: rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (hypothesis)
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 : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)
have h : (∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (hypothesis)
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 : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)
have 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))
Tactic: rw [← (Opposite.equivToOpposite (α := C)).forall_congr_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (hypothesis)
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))
⊢ (∀ (X : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)
have 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))
Tactic: rw [← (Opposite.equivToOpposite (α := D)).forall_congr_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Quadruple (goal)
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
⊢ Epi q.leftTriple.leftToRight ↔ Mono q.rightTriple.rightToLeft
have rw : (∀ (k : C), Epi (q.leftTriple.leftToRight.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.rightToLeft.app k)
Tactic: rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]
-- 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
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
X : C
⊢ NatTrans.app (unit (reflectorAdjunction i)) (i.obj ((reflector i).obj X)) =
    i.map ((reflector i).map (NatTrans.app (unit (reflectorAdjunction i)) X))
have 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))
Tactic: rw [← cancel_mono (i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X))),
    ← i.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
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)
⊢ i.essImage A
have this : 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 _))
-- 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
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)
have refine : Epi (retraction (η.app A) ≫ η.app A)
Tactic: refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.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
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 (retraction (η.app A) ≫ η.app A)
have rw : Epi (η.app ((reflector i ⋙ i).obj A) ≫ (reflector i ⋙ i).map (retraction (η.app A)))
Tactic: rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]
-- 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
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)))
⊢ i.essImage A
have this₁ : Epi (η.app A)
Tactic: have : Epi (η.app A) := by
    refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.app A) ?_
    rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]
    apply epi_comp (η.app (i.obj ((reflector i).obj A)))
-- 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
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A : C
inst_3 : IsSplitMono (Y := (reflector i ⋙ i).obj A) (NatTrans.app (unit (reflectorAdjunction i)) A)
η : 𝟭 C ⟶ reflector i ⋙ i := unit (reflectorAdjunction i)
this_1 :
  IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (i.obj ((reflector i).obj A))) (η.app (i.obj ((reflector i).obj A)))
this : Epi (η.app A)
⊢ i.essImage A
have this₁ : IsIso (η.app A)
Tactic: haveI := isIso_of_epi_of_isSplitMono (η.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
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
⊢ Eq (α := i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB' : (a : A ⟶ B') → i.obj ((reflector i).obj A) ⟶ B') (f ≫ h) :
      i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
      i.obj ((reflector i).obj A) ⟶ B')
have rw : f ≫ h =
  (Equiv.symm (unitCompPartialBijective A hB') : (a : i.obj ((reflector i).obj A) ⟶ B') → A ⟶ B')
    ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
      i.obj ((reflector i).obj A) ⟶ B')
Tactic: rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h hB, Equiv.symm_apply_apply]
-- 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
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
rw :
  f ≫ h =
    (Equiv.symm (unitCompPartialBijective A hB') : (a : i.obj ((reflector i).obj A) ⟶ B') → A ⟶ B')
      ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
        i.obj ((reflector i).obj A) ⟶ B')
⊢ Eq (α := i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB' : (a : A ⟶ B') → i.obj ((reflector i).obj A) ⟶ B') (f ≫ h) :
      i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
      i.obj ((reflector i).obj A) ⟶ B')
have rw₁ : f ≫ h =
  (Equiv.symm (unitCompPartialBijective A hB) : (a : i.obj ((reflector i).obj A) ⟶ B) → A ⟶ B)
      ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f :
        i.obj ((reflector i).obj A) ⟶ B) ≫
    h
Tactic: rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h hB, Equiv.symm_apply_apply]
-- 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
i : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
rw :
  f ≫ h =
    (Equiv.symm (unitCompPartialBijective A hB') : (a : i.obj ((reflector i).obj A) ⟶ B') → A ⟶ B')
      ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
        i.obj ((reflector i).obj A) ⟶ B')
rw₁ :
  f ≫ h =
    (Equiv.symm (unitCompPartialBijective A hB) : (a : i.obj ((reflector i).obj A) ⟶ B) → A ⟶ B)
        ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f :
          i.obj ((reflector i).obj A) ⟶ B) ≫
      h
⊢ Eq (α := i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB' : (a : A ⟶ B') → i.obj ((reflector i).obj A) ⟶ B') (f ≫ h) :
      i.obj ((reflector i).obj A) ⟶ B')
    ((unitCompPartialBijective A hB : (a : A ⟶ B) → i.obj ((reflector i).obj A) ⟶ B) f ≫ h :
      i.obj ((reflector i).obj A) ⟶ B')
have rw₂ : f ≫ h = f ≫ h
Tactic: rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h hB, Equiv.symm_apply_apply]