awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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))
⊢ 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) ≫ 𝟙 (U.obj (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))
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))
rw₃ :
  F'.map (adj₂.unit.app (U.1 X) ≫ 𝟙 (U.obj (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₂.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))
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))
rw₃ :
  F'.map (adj₂.unit.app (U.1 X) ≫ 𝟙 (U.obj (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.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₅ : Eq.{v₁ + 1} (α := F'.obj (U.obj X) ⟶ F'.obj (U.obj X)) (𝟙 (F'.obj (U.obj 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
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ Equiv.{v₁ + 1, max 1 (v₃ + 1)}
    { f : F'.obj (U.obj X) ⟶ Y // F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f }
    { g : U.obj X ⟶ U.obj (R.obj Y) // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g }
have apply : ∀ (a : F'.obj (U.obj X) ⟶ Y),
  F'.map (U.map (adj₁.counit.app X)) ≫ a = otherMap R F' adj₁ adj₂ X ≫ a ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
              a) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
          a)
Tactic: apply (adj₂.homEquiv _ _).subtypeEquiv _
-- 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
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
          f)
have rw : U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
    U.map (adj₁.counit.app X) ≫
      ((adj₂.homEquiv (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) Y :
            Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) ⟶ Y)
              (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X) ⟶ (R ⋙ U).obj Y)) :
          (a : F'.obj (U.obj ((𝟭 B).obj X)) ⟶ Y) → U.obj ((𝟭 B).obj X) ⟶ (R ⋙ U).obj Y)
        f ↔
  Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
    (U.map
      (F.map
          (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
              (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
            f) ≫
        adj₁.counit.app (R.obj Y)))
    (U.map (adj₁.counit.app X) ≫
      ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
          (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
        f)
Tactic: rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left,
        otherMap, assoc, adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality,
        adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit, adj₂.right_triangle_components,
        comp_id, Functor.comp_map, ← U.map_comp, assoc]
-- 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
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) Y :
              Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) ⟶ Y)
                (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X) ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj ((𝟭 B).obj X)) ⟶ Y) → U.obj ((𝟭 B).obj X) ⟶ (R ⋙ U).obj Y)
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
          f)
have dsimp : U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
    U.map (adj₁.counit.app X) ≫
      ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
          (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
        f ↔
  Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (R.obj Y))
    (U.map
      (F.map
          (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
              (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
            f) ≫
        adj₁.counit.app (R.obj Y)))
    (U.map (adj₁.counit.app X) ≫
      ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
          (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
        f)
Tactic: dsimp
-- 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
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (R.obj Y))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f)
have rw : U.map (F.map (adj₂.unit.app (U.1 X)) ≫ F.map (U.map (R.map f)) ≫ adj₁.counit.app (R.obj Y)) =
    U.map (adj₁.counit.app X) ≫
      ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
          (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
        f ↔
  Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (R.obj Y))
    (U.map
      (F.map
          (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
              (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
            f) ≫
        adj₁.counit.app (R.obj Y)))
    (U.map (adj₁.counit.app X) ≫
      ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
          (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
        f)
Tactic: rw [← adj₁.counit_naturality]
-- 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
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ Equiv.{v₃ + 1, max 1 (v₂ + 1)}
    { g : U.obj X ⟶ U.obj (R.obj Y) // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g }
    { z : F.obj (U.obj X) ⟶ R.obj Y // F.map (U.map (adj₁.counit.app X)) ≫ z = adj₁.counit.app ((U ⋙ F).obj X) ≫ z }
have apply : ∀ (a : U.obj X ⟶ U.obj (R.obj Y)),
  U.map (F.map a ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ a ↔
    Eq (α := F.obj (U.obj ((U ⋙ F).obj X)) ⟶ R.obj Y)
      (F.map (U.map (adj₁.counit.app X)) ≫
        ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
              Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
            (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
          a)
      (adj₁.counit.app ((U ⋙ F).obj X) ≫
        ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
              Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
            (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
          a)
Tactic: apply (adj₁.homEquiv _ _).symm.subtypeEquiv
-- 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
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g ↔
    Eq (α := F.obj (U.obj ((U ⋙ F).obj X)) ⟶ R.obj Y)
      (F.map (U.map (adj₁.counit.app X)) ≫
        ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
              Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
            (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
          g)
      (adj₁.counit.app ((U ⋙ F).obj X) ≫
        ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
              Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
            (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
          g)
have rw : adj₁.counit.app (F.obj (U.obj X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) =
    F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)) ↔
  F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) =
    adj₁.counit.app ((U ⋙ F).obj X) ≫ F.map g ≫ adj₁.counit.app (R.obj Y)
Tactic: rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit,
        adj₁.homEquiv_counit, adj₁.homEquiv_counit, F.map_comp, assoc, U.map_comp, F.map_comp,
        assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]
-- 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
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
⊢ Functor.{v₂, v₁, u₂, u₁} B A
have refine : ∀ (X : B) (Y Y' : A) (g : Y ⟶ Y') (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
  Eq.{v₂ + 1} (α := X ⟶ R.obj Y')
    ((((fun (X : B) (Y : A) ↦
                (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X :
                  Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)))
              X Y' :
            Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y') (X ⟶ R.obj Y')) :
          (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y') → X ⟶ R.obj Y')
        (h_1 ≫ g) :
      X ⟶ R.obj Y')
    ((((fun (X : B) (Y : A) ↦
                  (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X :
                    Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)))
                X Y :
              Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)) :
            (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) → X ⟶ R.obj Y)
          h_1 ≫
        R.map g :
      X ⟶ R.obj Y')
Tactic: refine Adjunction.leftAdjointOfEquiv (fun X Y => constructLeftAdjointEquiv R _ adj₁ adj₂ h Y 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
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
⊢ R.IsRightAdjoint
have rsuffices : R'.IsRightAdjoint → R.IsRightAdjoint
Tactic: rsuffices : R'.IsRightAdjoint
-- 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
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
rsuffices : R'.IsRightAdjoint → R.IsRightAdjoint
⊢ R.IsRightAdjoint
have rsuffices₁ : R'.IsRightAdjoint
Tactic: rsuffices : R'.IsRightAdjoint
-- 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
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
this_1 : R'.IsRightAdjoint
this : (R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U))).IsRightAdjoint := ⋯
⊢ R.IsRightAdjoint
have refine : R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U)) ≅ R
Tactic: refine ((Adjunction.ofIsRightAdjoint
      (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv)).ofNatIsoRight ?_).isRightAdjoint
-- 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
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
⊢ (R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget).IsRightAdjoint
have refine : R ⋙ U ≅ R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget
Tactic: refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint
-- 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
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget).IsRightAdjoint := ⋯
X : (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra
⊢ RegularEpi ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).adj.counit.app X)
have simp : RegularEpi (C := (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) (X :=
  ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget ⋙
        (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).free).obj
    X)
  (Y := Functor.obj (𝟭 (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) X)
  { f := X.a, h := sorry : ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).free.obj X.A).Hom X }
Tactic: simp only [Monad.adj_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (hypothesis)
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₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
⊢ { l : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }
have this : ∀ (Y : B), Mono (adj₁.unit.app Y)
Tactic: have := fun Y ↦ h Y |>.mono