awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
K : Functor.{v, v₂, u, u₂} J D
inst_3 : ComonadicLeftAdjoint R
inst_4 : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst_5 : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra :=
  Comonad.comparison (comonadicAdjunction R)
B : (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra ⥤ C :=
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙
    (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≅
  K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R))
      (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
this_1 : PreservesLimit ((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget)
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).toFunctor :=
  ⋯
this_2 : PreservesLimit
  (((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget) ⋙
    (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).toFunctor)
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).toFunctor :=
  ⋯
this_3 : CreatesLimit (K ⋙ A) B := Comonad.forgetCreatesLimit (K ⋙ A)
this : CreatesLimit K (A ⋙ B) := compCreatesLimit A B
e : Comonad.comparison (comonadicAdjunction R) ⋙
    (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≅
  R :=
  Comonad.comparisonForget (comonadicAdjunction R)
⊢ CreatesLimit K R

Tactic:
apply createsLimitOfNatIso e

Premises used: CategoryTheory.createsLimitOfNatIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : ComonadicLeftAdjoint R
inst_4 : PreservesLimitsOfShape.{v, u, v₂, v₁, u₂, u₁} J R
⊢ PreservesLimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (comonadicRightAdjoint R)

Tactic:
apply (Adjunction.rightAdjoint_preservesLimits (comonadicAdjunction R)).1

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : ComonadicLeftAdjoint R
inst_4 : PreservesLimitsOfShape.{v, u, v₂, v₁, u₂, u₁} J R
this : PreservesLimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (comonadicRightAdjoint R) := ⋯
⊢ PreservesLimitsOfShape.{v, u, v₁, v₁, u₁, u₁} J (comonadicRightAdjoint R ⋙ R)

Tactic:
apply CategoryTheory.Limits.comp_preservesLimitsOfShape _ _

Premises used: CategoryTheory.Limits.comp_preservesLimitsOfShape
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
F : Functor.{v, v₂, u, u₂} J D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : HasColimit (F ⋙ R)
inst_4 : Coreflective R
⊢ HasColimit F

Tactic:
haveI := comonadicCreatesColimits.{v, u} R
  hasColimit_of_created F R

Premises used: CategoryTheory.hasColimit_of_created
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
inst_3 : HasColimitsOfShape.{v, u, v₁, u₁} J C
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : Coreflective R
⊢ HasColimitsOfShape.{v, u, v₂, u₂} J D

Tactic:
⟨fun F => hasColimit_of_coreflective F R⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.hasColimit_of_coreflective
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_3 : Coreflective R
⊢ HasColimitsOfSize.{v, u, v₂, u₂} D

Tactic:
⟨fun _ => hasColimitsOfShape_of_coreflective R⟩

Premises used: CategoryTheory.hasColimitsOfShape_of_coreflective, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : Coreflective R
inst_4 : HasLimitsOfShape.{v, u, v₁, u₁} J C
F : Functor.{v, v₂, u, u₂} J D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (comonadicRightAdjoint R) := ⋯
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
apply : (F ⋙ R) ⋙ comonadicRightAdjoint R ≅ F
⊢ HasLimit F

Tactic:
apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : Coreflective R
inst_4 : HasLimitsOfShape.{v, u, v₁, u₁} J C
F : Functor.{v, v₂, u, u₂} J D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (comonadicRightAdjoint R) := ⋯
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ (F ⋙ R) ⋙ comonadicRightAdjoint R ≅ F

Tactic:
apply
        (F.rightUnitor ≪≫ (isoWhiskerLeft F ((asIso (comonadicAdjunction R).unit) :))).symm

Premises used: CategoryTheory.Functor.rightUnitor, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.comonadicAdjunction, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
inst_3 : HasLimitsOfSize.{v, u, v₁, u₁} C
⊢ HasLimitsOfSize.{v, u, v₂, u₂} D

Tactic:
⟨fun _ => hasLimitsOfShape_of_coreflective R⟩

Premises used: CategoryTheory.hasLimitsOfShape_of_coreflective, CategoryTheory.Limits.HasLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
preserves : ∀ {c : Cocone (F ⋙ R)} (hc : IsColimit c), Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
⊢ PreservesColimit (F ⋙ R) (comonadicRightAdjoint R)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
⊢ HasColimit (F ⋙ R)

Tactic:
haveI : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this : HasColimit (F ⋙ R)
⊢ HasColimit F

Tactic:
haveI : HasColimit F := hasColimit_of_coreflective F R
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
preserves : IsColimit ((comonadicRightAdjoint R).mapCocone c)
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
preserves : (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt
⊢ IsColimit ((comonadicRightAdjoint R).mapCocone c)

Tactic:
apply isColimitChangeEmptyCocone D (colimit.isColimit F)

Premises used: CategoryTheory.Limits.isColimitChangeEmptyCocone, CategoryTheory.Limits.colimit.isColimit
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
preserves : (R ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone c).pt
⊢ (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt

Tactic:
apply (asIso ((comonadicAdjunction R).unit.app _)).trans

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Iso.trans, CategoryTheory.comonadicAdjunction, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
preserves : R.obj (colimit.cocone F).1 ≅ c.pt
⊢ (R ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone c).pt

Tactic:
apply (comonadicRightAdjoint R).mapIso

Premises used: CategoryTheory.comonadicRightAdjoint, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this_2 : HasColimit F
this : CreatesColimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := comonadicCreatesColimits R
A : PreservesColimit F R := ⋯
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Tactic:
apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
this : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) := ⋯
⊢ PreservesColimit K (comonadicRightAdjoint R)

Tactic:
apply preservesColimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)

Premises used: CategoryTheory.Functor.emptyExt, CategoryTheory.Functor.comp, CategoryTheory.Limits.preservesColimit_of_iso_diagram
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
apply : F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
apply₁ : F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
⊢ IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))

Tactic:
apply IsReflexivePair.mk' (F.map (adj.unit.app _)) _ _

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.IsReflexivePair.mk', CategoryTheory.Functor.map, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
rw : F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
⊢ F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))

Tactic:
rw [← F.map_comp, ← F.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))

Tactic:
congr_arg F.map A.unit

Premises used: CategoryTheory.Functor.map, congr_arg, CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))

Tactic:
exact congr_arg F.map A.unit

Premises used: CategoryTheory.Functor.map, congr_arg, CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
dsimp : F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj A.A)
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
rw rw₁ : Eq.{v₁ + 1} (α := F.obj A.A ⟶ F.obj A.A) (𝟙 (F.obj A.A)) (𝟙 (F.obj A.A))
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj A.A)

Tactic:
rw [adj.left_triangle_components]

Premises used: CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
refine :
  ∀ (a : F.obj A.A ⟶ B),
    F.map A.a ≫ a = adj.counit.app (F.obj A.A) ≫ a ↔
      G.map (F.map ((adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) a)) ≫ G.map (adj.counit.app B) =
        A.a ≫ (adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) a
⊢ { f : F.obj A.A ⟶ B // F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f } ≃
    { g : A.A ⟶ G.obj B // G.map (F.map g) ≫ G.map (adj.counit.app B) = A.a ≫ g }

Tactic:
refine (adj.homEquiv _ _).subtypeEquiv ?_

Premises used: Equiv.subtypeEquiv, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
rw :
  A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
⊢ F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f ↔
    G.map (F.map ((adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) f)) ≫ G.map (adj.counit.app B) =
      A.a ≫ (adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) f

Tactic:
rw [← (adj.homEquiv _ _).injective.eq_iff, Adjunction.homEquiv_naturality_left,
        adj.homEquiv_unit, adj.homEquiv_unit, G.map_comp]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, Function.Injective.eq_iff, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.homEquiv, Equiv.injective, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
dsimp :
  A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (G.obj (F.obj A.A)) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
rw : A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔ G.map f = A.a ≫ adj.unit.app A.A ≫ G.map f
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (G.obj (F.obj A.A)) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
rw [adj.right_triangle_components_assoc, ← G.map_comp, F.map_comp, Category.assoc,
        adj.counit_naturality, adj.left_triangle_components_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components_assoc, CategoryTheory.Adjunction.left_triangle_components_assoc
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔ G.map f = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
apply eq_comm

Premises used: eq_comm
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
refine_1 :
  (A : adj.toMonad.Algebra) →
    (B : D) → ((fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)
refine_2 :
  ∀ (X : adj.toMonad.Algebra) (Y Y' : D) (g : Y ⟶ Y')
    (h : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) X ⟶ Y),
    Eq (α := X ⟶ (comparison adj).obj Y')
      (((fun (A : adj.toMonad.Algebra) (B : D) ↦
                (comparisonLeftAdjointHomEquiv adj A B :
                  (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)))
              X Y' :
            (a : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) X ⟶ Y') → X ⟶ (comparison adj).obj Y')
          (h ≫ g) :
        X ⟶ (comparison adj).obj Y')
      (((fun (A : adj.toMonad.Algebra) (B : D) ↦
                  (comparisonLeftAdjointHomEquiv adj A B :
                    (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)))
                X Y :
              (a : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) X ⟶ Y) → X ⟶ (comparison adj).obj Y)
            h ≫
          (comparison adj).map g :
        X ⟶ (comparison adj).obj Y')
⊢ adj.toMonad.Algebra ⥤ D

Tactic:
refine
    Adjunction.leftAdjointOfEquiv (G := comparison adj)
      (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_

Premises used: CategoryTheory.Adjunction.leftAdjointOfEquiv
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B : D
⊢ ((fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)

Tactic:
apply comparisonLeftAdjointHomEquiv

Premises used: CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B B' : D
g : B ⟶ B'
h : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B
refine_2 :
  Eq.{v₁ + 1} (α := A.A ⟶ ((comparison adj).obj B').A)
    (Algebra.Hom.f
      (((fun (A : adj.toMonad.Algebra) (B : D) ↦
              (comparisonLeftAdjointHomEquiv adj A B :
                (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)))
            A B' :
          (a : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B') → A ⟶ (comparison adj).obj B')
        (h ≫ g)))
    (Algebra.Hom.f
      (((fun (A : adj.toMonad.Algebra) (B : D) ↦
                (comparisonLeftAdjointHomEquiv adj A B :
                  (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)))
              A B :
            (a : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B) → A ⟶ (comparison adj).obj B)
          h ≫
        (comparison adj).map g))
⊢ Eq (α := A ⟶ (comparison adj).obj B')
    (((fun (A : adj.toMonad.Algebra) (B : D) ↦
              (comparisonLeftAdjointHomEquiv adj A B :
                (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)))
            A B' :
          (a : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B') → A ⟶ (comparison adj).obj B')
        (h ≫ g) :
      A ⟶ (comparison adj).obj B')
    (((fun (A : adj.toMonad.Algebra) (B : D) ↦
                (comparisonLeftAdjointHomEquiv adj A B :
                  (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)))
              A B :
            (a : (fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B) → A ⟶ (comparison adj).obj B)
          h ≫
        (comparison adj).map g :
      A ⟶ (comparison adj).obj B')

Tactic:
ext1