awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
_ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
_₁ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
    ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y))
_₂ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (Δ ≫ (f ⊗ₘ f))
have _₃ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y))
Tactic: calc
    _ = f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y) := by
      cat_disch
    _ = (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) := by
      rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
      simp
    _ = Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = Δ ≫ ((𝟙 X ≫ f) ⊗ₘ (f ≫ 𝟙 Y)) := by
      rw [MonoidalCategory.tensorHom_comp_tensorHom]
    _ = Δ ≫ (f ⊗ₘ f) := by cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
_ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
_₁ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
    ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y))
_₂ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
_₃ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y))
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (Δ ≫ (f ⊗ₘ f))
have _₄ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y))
Tactic: calc
    _ = f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y) := by
      cat_disch
    _ = (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) := by
      rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
      simp
    _ = Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = Δ ≫ ((𝟙 X ≫ f) ⊗ₘ (f ≫ 𝟙 Y)) := by
      rw [MonoidalCategory.tensorHom_comp_tensorHom]
    _ = Δ ≫ (f ⊗ₘ f) := by cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
_ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
_₁ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
    ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y))
_₂ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
_₃ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y))
_₄ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y))
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (Δ ≫ (f ⊗ₘ f))
have _₅ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y)) (Δ ≫ (f ⊗ₘ f))
Tactic: calc
    _ = f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y) := by
      cat_disch
    _ = (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) := by
      rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
      simp
    _ = Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = Δ ≫ ((𝟙 X ≫ f) ⊗ₘ (f ≫ 𝟙 Y)) := by
      rw [MonoidalCategory.tensorHom_comp_tensorHom]
    _ = Δ ≫ (f ⊗ₘ f) := by cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ (L ⋙ R).map ((whiskerRight (L.whiskerLeft h.counit) R).app X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X =
    (whiskerRight (L.whiskerLeft h.counit) R).app ((L ⋙ R).obj X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X
have dsimp : Eq (α := R.obj (L.obj (R.obj (L.obj (R.obj (L.obj X))))) ⟶ R.obj (L.obj X))
  (R.map (L.map (R.map (h.counit.app (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
  (R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ Eq (α := R.obj (L.obj (R.obj (L.obj (R.obj (L.obj X))))) ⟶ R.obj (L.obj X))
    (R.map (L.map (R.map (h.counit.app (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
    (R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
have rw : Eq (α := R.obj (L.obj (R.obj (L.obj (R.obj (L.obj X))))) ⟶ R.obj (L.obj X))
  (R.map (L.map (R.map (h.counit.app (L.obj X))) ≫ h.counit.app (L.obj X)))
  (R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
Tactic: rw [← R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ (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))
have dsimp : R.map (L.map (h.unit.app X)) ≫ R.map (h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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)) ≫ R.map (h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
have rw : R.map (L.map (h.unit.app X) ≫ h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
Tactic: rw [← R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ (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)
have 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)))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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)) ≫ 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)))))
have 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)))))
Tactic: rw [← L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ (whiskerRight (R.whiskerLeft h.unit) L).app X ≫ (R ⋙ L).map (h.counit.app X) = 𝟙 ((R ⋙ L).obj X)
have dsimp : L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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)) ≫ L.map (R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
have rw : L.map (h.unit.app (R.obj X) ≫ R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
Tactic: rw [← L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ adj.unit ≫ i.hom ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)
have rw : (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)
Tactic: rw [← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)
have w : ∀ (X : C), ((adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ).app X = NatTrans.app (𝟙 (𝟭 C)) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ (i.hom ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ) ≫ adj.unit = 𝟙 (L ⋙ R)
have rw : (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport (F := 𝟭 C) i).μ = 𝟙 (𝟭 C)
Tactic: rw [assoc, ← Iso.eq_inv_comp, comp_id, ← id_comp i.inv, Iso.eq_comp_inv, assoc,
      NatTrans.id_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ adj.counit ≫ (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv = 𝟙 (R ⋙ L)
have rw : (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)
Tactic: rw [← assoc, Iso.comp_inv_eq, id_comp, ← comp_id j.hom, ← Iso.inv_comp_eq, ← assoc,
      NatTrans.id_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)
have w : ∀ (X : D), ((adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit).app X = NatTrans.app (𝟙 (𝟭 D)) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ ((adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv) ≫ adj.counit = 𝟙 (𝟭 D)
have rw : (adj.toComonad.transport (F := 𝟭 D) j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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)
have 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)
Tactic: rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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
have dsimp : R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f
have rw : R.map (L.map (R.map f) ≫ h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f
Tactic: rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f
have rw₁ : R.map (h.counit.app X ≫ f) = R.map (h.counit.app X) ≫ R.map f
Tactic: rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y) = R.map (h.counit.app X) ≫ R.map f
have rw₂ : R.map (h.counit.app X) ≫ R.map f = R.map (h.counit.app X) ≫ R.map f
Tactic: rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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))
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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 := ⋯ }
have dsimp : L.map (h.unit.app X) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y)
have rw : L.map (h.unit.app X ≫ R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y)
Tactic: rw [← L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A = 𝟙 ((reflector R ⋙ R).obj X.A)
have 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)
Tactic: rw [← (reflectorAdjunction R).unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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)
have 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))
Tactic: dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ 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))
have rw : R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫ X.a)) =
  𝟙 (R.obj ((reflector R).obj X.A))
Tactic: rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A) ≅ X
have symm : X ≅ obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
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
⊢ X ≅ obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)
have refine_1 : X.A ≅
  Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
    (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))
Tactic: refine Monad.Algebra.isoMk ?_ ?_