awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
dsimp : R.map (L.map (h.unit.app X)) ≫ R.map (h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
⊢ (L ⋙ R).map (h.unit.app X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X =
    𝟙 ((L ⋙ R).obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
rw : R.map (L.map (h.unit.app X) ≫ h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
⊢ R.map (L.map (h.unit.app X)) ≫ R.map (h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))

Tactic:
rw [← R.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
⊢ R.map (L.map (h.unit.app X) ≫ h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
dsimp :
  Eq (α := L.obj (R.obj X) ⟶ L.obj (R.obj (L.obj (R.obj (L.obj (R.obj X))))))
    (L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (L.map (h.unit.app (R.obj X)))))
    (L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X)))))
⊢ (whiskerRight (R.whiskerLeft h.unit) L).app X ≫ (R ⋙ L).map ((whiskerRight (R.whiskerLeft h.unit) L).app X) =
    (whiskerRight (R.whiskerLeft h.unit) L).app X ≫ (whiskerRight (R.whiskerLeft h.unit) L).app ((R ⋙ L).obj X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
rw :
  Eq (α := L.obj (R.obj X) ⟶ L.obj (R.obj (L.obj (R.obj (L.obj (R.obj X))))))
    (L.map (h.unit.app (R.obj X) ≫ R.map (L.map (h.unit.app (R.obj X)))))
    (L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X)))))
⊢ Eq (α := L.obj (R.obj X) ⟶ L.obj (R.obj (L.obj (R.obj (L.obj (R.obj X))))))
    (L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (L.map (h.unit.app (R.obj X)))))
    (L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X)))))

Tactic:
rw [← L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
⊢ Eq (α := L.obj (R.obj X) ⟶ L.obj (R.obj (L.obj (R.obj (L.obj (R.obj X))))))
    (L.map (h.unit.app (R.obj X) ≫ R.map (L.map (h.unit.app (R.obj X)))))
    (L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
dsimp : L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
⊢ (whiskerRight (R.whiskerLeft h.unit) L).app X ≫ (R ⋙ L).map (h.counit.app X) = 𝟙 ((R ⋙ L).obj X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
rw : L.map (h.unit.app (R.obj X) ≫ R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
⊢ L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))

Tactic:
rw [← L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
⊢ L.map (h.unit.app (R.obj X) ≫ R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
rw : (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)
⊢ adj.unit ≫ i.hom ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)

Tactic:
rw [← assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
w : ∀ (X : C), ((adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ).app X = NatTrans.app (𝟙 (𝟭 C)) X
⊢ (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
X : C
⊢ ((adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ).app X = NatTrans.app (𝟙 (𝟭 C)) X

Tactic:
(adj.toMonad.transport i).right_unit X

Premises used: CategoryTheory.Monad.right_unit, CategoryTheory.Monad.transport, CategoryTheory.Adjunction.toMonad
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
X : C
⊢ ((adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ).app X = NatTrans.app (𝟙 (𝟭 C)) X

Tactic:
exact (adj.toMonad.transport i).right_unit X

Premises used: CategoryTheory.Monad.right_unit, CategoryTheory.Monad.transport, CategoryTheory.Adjunction.toMonad
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
rw : (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)
⊢ (i.hom ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ) ≫ adj.unit = 𝟙 (L ⋙ R)

Tactic:
rw [assoc, ← Iso.eq_inv_comp, comp_id, ← id_comp i.inv, Iso.eq_comp_inv, assoc,
      NatTrans.id_comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.id_comm, CategoryTheory.Iso.eq_inv_comp, CategoryTheory.Iso.inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ IsIso adj.unit

Tactic:
(inferInstanceAs (IsIso (unitAsIsoOfIso adj i).hom))

Premises used: _private.0.CategoryTheory.Adjunction.isIso_unit_of_iso._proof_1
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
rw : (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)
⊢ adj.counit ≫ (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv = 𝟙 (R ⋙ L)

Tactic:
rw [← assoc, Iso.comp_inv_eq, id_comp, ← comp_id j.hom, ← Iso.inv_comp_eq, ← assoc,
      NatTrans.id_comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.id_comm, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
w : ∀ (X : D), ((adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit).app X = NatTrans.app (𝟙 (𝟭 D)) X
⊢ (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
X : D
⊢ ((adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit).app X = NatTrans.app (𝟙 (𝟭 D)) X

Tactic:
(adj.toComonad.transport j).right_counit X

Premises used: CategoryTheory.Comonad.right_counit, CategoryTheory.Adjunction.toComonad, CategoryTheory.Comonad.transport
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
X : D
⊢ ((adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit).app X = NatTrans.app (𝟙 (𝟭 D)) X

Tactic:
exact (adj.toComonad.transport j).right_counit X

Premises used: CategoryTheory.Comonad.right_counit, CategoryTheory.Adjunction.toComonad, CategoryTheory.Comonad.transport
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
rw : (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)
⊢ ((adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv) ≫ adj.counit = 𝟙 (𝟭 D)

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ IsIso adj.counit

Tactic:
inferInstanceAs (IsIso (counitAsIsoOfIso adj j).hom)

Premises used: _private.0.CategoryTheory.Adjunction.isIso_counit_of_iso._proof_1
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
dsimp :
  R.map (h.counit.app (L.obj (R.obj X))) ≫ R.map (h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
⊢ h.toMonad.μ.app (R.obj X) ≫ R.map (h.counit.app X) = h.toMonad.map (R.map (h.counit.app X)) ≫ R.map (h.counit.app X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
rw :
  R.map (h.counit.app (L.obj (R.obj X)) ≫ h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
rw₁ :
  R.map (L.map (R.map (h.counit.app X)) ≫ h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
rw₂ rw₃ :
  R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
⊢ R.map (h.counit.app (L.obj (R.obj X))) ≫ R.map (h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)

Tactic:
rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]

Premises used: CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X Y : D
f : X ⟶ Y
dsimp : R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f
⊢ h.toMonad.map (R.map f) ≫ { A := R.obj Y, a := R.map (h.counit.app Y), unit := ⋯, assoc := ⋯ : h.toMonad.Algebra }.a =
    { A := R.obj X, a := R.map (h.counit.app X), unit := ⋯, assoc := ⋯ : h.toMonad.Algebra }.a ≫ R.map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X Y : D
f : X ⟶ Y
rw : R.map (L.map (R.map f) ≫ h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f
rw₁ : R.map (h.counit.app X ≫ f) = R.map (h.counit.app X) ≫ R.map f
rw₂ rw₃ : R.map (h.counit.app X) ≫ R.map f = R.map (h.counit.app X) ≫ R.map f
⊢ R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f

Tactic:
rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp]

Premises used: CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
⊢ L ⋙ comparison h = h.toMonad.free

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Monad.free, rfl
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
T : Monad.{v₁, u₁} C
x x_1 : T.Algebra
f : (Monad.comparison T.adj).obj x ⟶ (Monad.comparison T.adj).obj x_1
⊢ T.map f.f ≫ x_1.a = x.a ≫ f.f

Tactic:
simpa using f.h

Premises used: CategoryTheory.Monad.Algebra.Hom.h
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
T : Monad.{v₁, u₁} C
X : T.adj.toMonad.Algebra
⊢ T.η.app X.A ≫ X.a = 𝟙 X.A

Tactic:
simpa using X.unit

Premises used: CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
T : Monad.{v₁, u₁} C
X : T.adj.toMonad.Algebra
⊢ T.μ.app X.A ≫ X.a = T.map X.a ≫ X.a

Tactic:
simpa using X.assoc

Premises used: CategoryTheory.Monad.Algebra.assoc
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
dsimp :
  L.map (h.unit.app X) ≫ L.map (h.unit.app (R.obj (L.obj X))) =
    L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))
⊢ L.map (h.unit.app X) ≫ h.toComonad.δ.app (L.obj X) = L.map (h.unit.app X) ≫ h.toComonad.map (L.map (h.unit.app X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
rw : L.map (h.unit.app X ≫ h.unit.app (R.obj (L.obj X))) = L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))
rw₁ : L.map (h.unit.app X ≫ R.map (L.map (h.unit.app X))) = L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))
rw₂ rw₃ :
  L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X))) =
    L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))
⊢ L.map (h.unit.app X) ≫ L.map (h.unit.app (R.obj (L.obj X))) =
    L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))

Tactic:
rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]

Premises used: CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X Y : C
f : X ⟶ Y
dsimp : L.map (h.unit.app X) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y)
⊢ Coalgebra.a { A := L.obj X, a := L.map (h.unit.app X), counit := ⋯, coassoc := ⋯ : h.toComonad.Coalgebra } ≫
      h.toComonad.map (L.map f) =
    L.map f ≫ Coalgebra.a { A := L.obj Y, a := L.map (h.unit.app Y), counit := ⋯, coassoc := ⋯ }

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X Y : C
f : X ⟶ Y
rw : L.map (h.unit.app X ≫ R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y)
⊢ L.map (h.unit.app X) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y)

Tactic:
rw [← L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X Y : C
f : X ⟶ Y
⊢ L.map (h.unit.app X ≫ R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
⊢ R ⋙ comparison h = h.toComonad.cofree

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Comonad.cofree, rfl
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
G : Comonad.{v₁, u₁} C
X Y : G.Coalgebra
f : (Comonad.comparison G.adj).obj X ⟶ (Comonad.comparison G.adj).obj Y
⊢ X.a ≫ G.map f.f = f.f ≫ Y.a

Tactic:
simpa using f.h

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.h
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
G : Comonad.{v₁, u₁} C
X : G.adj.toComonad.Coalgebra
⊢ X.a ≫ G.ε.app X.A = 𝟙 X.A

Tactic:
simpa using X.counit

Premises used: CategoryTheory.Comonad.Coalgebra.counit
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
G : Comonad.{v₁, u₁} C
X : G.adj.toComonad.Coalgebra
⊢ X.a ≫ G.δ.app X.A = X.a ≫ G.map X.a

Tactic:
simpa using X.coassoc

Premises used: CategoryTheory.Comonad.Coalgebra.coassoc
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R_1 R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : MonadicRightAdjoint R
⊢ IsEquivalence (D := (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).Algebra)
    (Monad.comparison (monadicAdjunction R))

Tactic:
MonadicRightAdjoint.eqv

Premises used: CategoryTheory.monadicLeftAdjoint, CategoryTheory.MonadicRightAdjoint.eqv, CategoryTheory.monadicAdjunction
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R_1 R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : MonadicRightAdjoint R
⊢ R.IsRightAdjoint

Tactic:
(monadicAdjunction R).isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.monadicAdjunction
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L_1 : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ComonadicLeftAdjoint L
⊢ IsEquivalence (D := (Adjunction.toComonad (R := comonadicRightAdjoint L) (comonadicAdjunction L)).Coalgebra)
    (Comonad.comparison (comonadicAdjunction L))

Tactic:
ComonadicLeftAdjoint.eqv

Premises used: CategoryTheory.ComonadicLeftAdjoint.eqv, CategoryTheory.comonadicRightAdjoint, CategoryTheory.comonadicAdjunction
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L_1 : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ComonadicLeftAdjoint L
⊢ L.IsLeftAdjoint

Tactic:
(comonadicAdjunction L).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.comonadicAdjunction
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
⊢ IsIso (X := (reflector R ⋙ R) ⋙ reflector R ⋙ R)
    (whiskerRight ((reflector R).whiskerLeft (Adjunction.counit (reflectorAdjunction R))) R)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
⊢ IsIso (Y := (coreflector R ⋙ R) ⋙ coreflector R ⋙ R)
    (whiskerRight ((coreflector R).whiskerLeft (Adjunction.unit (coreflectorAdjunction R))) R)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
dsimp : X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A = 𝟙 ((reflector R ⋙ R).obj X.A)
⊢ X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A = 𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.id_obj]

Premises used: CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
rw :
  NatTrans.app (Adjunction.unit (reflectorAdjunction R)) ((reflector R ⋙ R).obj X.A) ≫ R.map ((reflector R).map X.a) =
    𝟙 ((reflector R ⋙ R).obj X.A)
⊢ X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A = 𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
rw [← (reflectorAdjunction R).unit_naturality]

Premises used: CategoryTheory.reflectorAdjunction, CategoryTheory.Adjunction.unit_naturality
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
dsimp :
  NatTrans.app (Adjunction.unit (reflectorAdjunction R)) (R.obj ((reflector R).obj X.A)) ≫
      R.map ((reflector R).map X.a) =
    𝟙 (R.obj ((reflector R).obj X.A))
⊢ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) ((reflector R ⋙ R).obj X.A) ≫ R.map ((reflector R).map X.a) =
    𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Adjunction.toMonad_coe
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
rw :
  R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫ X.a)) =
    𝟙 (R.obj ((reflector R).obj X.A))
⊢ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) (R.obj ((reflector R).obj X.A)) ≫
      R.map ((reflector R).map X.a) =
    𝟙 (R.obj ((reflector R).obj X.A))

Tactic:
rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.unit_obj_eq_map_unit