awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
h : IsSplitEpi (T.ε.app X)
rw : T.ε.app X ≫ section_ (T.ε.app X) = T.map (𝟙 X)
rw₁ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X) ≫ T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)
have rw₂ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.map (T.ε.app X)
Tactic: rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X),
    map_comp, T.map_counit_app X, T.counit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
h : IsSplitEpi (T.ε.app X)
rw : T.ε.app X ≫ section_ (T.ε.app X) = T.map (𝟙 X)
rw₁ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X) ≫ T.ε.app X)
rw₂ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.map (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)
have rw₃ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.ε.app (T.obj X)
Tactic: rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X),
    map_comp, T.map_counit_app X, T.counit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
h : IsSplitEpi (T.ε.app X)
rw : T.ε.app X ≫ section_ (T.ε.app X) = T.map (𝟙 X)
rw₁ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X) ≫ T.ε.app X)
rw₂ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.map (T.ε.app X)
rw₃ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.ε.app (T.obj X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)
have rw₄ : T.ε.app X ≫ section_ (T.ε.app X) = T.ε.app X ≫ section_ (T.ε.app X)
Tactic: rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X),
    map_comp, T.map_counit_app X, T.counit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
have apply : T.free.obj X.A ⟶ T.free.obj (T.obj X.A)
Tactic: apply IsReflexivePair.mk' _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
apply : T.free.obj X.A ⟶ T.free.obj (T.obj X.A)
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
have apply₁ : T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)
Tactic: apply IsReflexivePair.mk' _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
apply : T.free.obj X.A ⟶ T.free.obj (T.obj X.A)
apply₁ : T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
have apply₂ : T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)
Tactic: apply IsReflexivePair.mk' _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)
have h : (T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X).f = Algebra.Hom.f (𝟙 (T.free.obj X.A))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ (T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X).f = Algebra.Hom.f (𝟙 (T.free.obj X.A))
have h : T.map (T.η.app X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ T.map (T.η.app X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)
have h : T.map (T.η.app X.A ≫ X.a) = 𝟙 (T.obj X.A)
Tactic: rw [← Functor.map_comp, X.unit, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
h : T.map (T.η.app X.A ≫ X.a) = 𝟙 (T.obj X.A)
⊢ T.map (T.η.app X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)
have h₁ : T.map (𝟙 X.A) = 𝟙 (T.obj X.A)
Tactic: rw [← Functor.map_comp, X.unit, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
h : T.map (T.η.app X.A ≫ X.a) = 𝟙 (T.obj X.A)
h₁ : T.map (𝟙 X.A) = 𝟙 (T.obj X.A)
⊢ T.map (T.η.app X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)
have h₂ : Eq.{v₁ + 1} (α := T.obj X.A ⟶ T.obj X.A) (𝟙 (T.obj X.A)) (𝟙 (T.obj X.A))
Tactic: rw [← Functor.map_comp, X.unit, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)
have h : (T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X).f = Algebra.Hom.f (𝟙 (T.free.obj X.A))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
⊢ { l : (beckAlgebraCofork X).pt ⟶ s.pt //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }
have h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
Tactic: have h₁ : (T : C ⥤ C).map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f :=
      congr_arg Monad.Algebra.Hom.f s.condition
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
⊢ { l : (beckAlgebraCofork X).pt ⟶ s.pt //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }
have h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
Tactic: have h₂ : (T : C ⥤ C).map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f := s.π.h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ { l : (beckAlgebraCofork X).pt ⟶ s.pt //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }
have refine_1 : T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
  (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
Tactic: refine ⟨⟨T.η.app _ ≫ s.π.f, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 :
  T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
⊢ { l : (beckAlgebraCofork X).pt ⟶ s.pt //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }
have refine_2 : (beckAlgebraCofork X).π ≫
    { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := sorry : (beckAlgebraCofork X).pt.Hom s.pt } =
  s.π
Tactic: refine ⟨⟨T.η.app _ ≫ s.π.f, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 :
  T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
refine_2 :
  (beckAlgebraCofork X).π ≫
      { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ : (beckAlgebraCofork X).pt.Hom s.pt } =
    s.π
⊢ { l : (beckAlgebraCofork X).pt ⟶ s.pt //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }
have refine_3 : ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt},
  (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := sorry }
Tactic: refine ⟨⟨T.η.app _ ≫ s.π.f, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
have refine_1 : T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
have refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
Tactic: rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
have refine_1₁ : T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
Tactic: rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₁ : T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
have refine_1₂ : T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
Tactic: rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₁ : T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₂ : T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
have refine_1₃ : s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
Tactic: rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₁ : T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₂ : T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₃ : s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
have refine_1₄ : s.π.f = T.η.app (T.obj X.1) ≫ T.map X.2 ≫ s.π.f
Tactic: rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₁ : T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₂ : T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₃ : s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₄ : s.π.f = T.η.app (T.obj X.1) ≫ T.map X.2 ≫ s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
have refine_1₅ : s.π.f = T.η.app (T.obj X.1) ≫ T.μ.app X.A ≫ s.π.f
Tactic: rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₁ : T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₂ : T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₃ : s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₄ : s.π.f = T.η.app (T.obj X.1) ≫ T.map X.2 ≫ s.π.f
refine_1₅ : s.π.f = T.η.app (T.obj X.1) ≫ T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
have refine_1₆ : s.π.f = s.π.f
Tactic: rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ (beckAlgebraCofork X).π ≫
      { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ : (beckAlgebraCofork X).pt.Hom s.pt } =
    s.π
have refine_2 : ((beckAlgebraCofork X).π ≫
      { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := sorry : (beckAlgebraCofork X).pt.Hom s.pt }).f =
  s.π.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }
have refine_3 : m.f = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := sorry }.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }.f
have refine_3 : m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Coequalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
have refine_3 : m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ ((beckAlgebraCofork X).π ≫ m).f
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))
have apply : G.map A.a ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
Tactic: apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
apply : G.map A.a ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
⊢ IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))
have apply₁ : adj.unit.app (G.obj A.A) ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
Tactic: apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ G.map A.a ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
have rw : G.map (A.a ≫ adj.counit.app A.1) = G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
Tactic: rw [← G.map_comp, ← G.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ adj.unit.app (G.obj A.A) ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
have rw : Eq.{v₁ + 1} (α := G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1) ⟶ G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
  (𝟙 (G.obj A.A)) (𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1)))
Tactic: rw [adj.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ B ⟶ comparisonRightAdjointObj adj A
have refine : Eq (α := B ⟶ G.obj (adj.toComonad.obj A.A))
  ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ G.map A.a : B ⟶ G.obj (adj.toComonad.obj A.A))
  ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ adj.unit.app (G.1 A.A) :
    B ⟶ G.obj (adj.toComonad.obj A.A))
Tactic: refine equalizer.lift (adj.homEquiv _ _ f.f) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ Eq (α := B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ G.map A.a : B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ adj.unit.app (G.1 A.A) :
      B ⟶ G.obj (adj.toComonad.obj A.A))
have simp : adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ (G ⋙ F).map f.f) = adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
Tactic: simp only [Adjunction.toComonad_coe, Functor.comp_obj, Adjunction.homEquiv_unit,
          Category.assoc, ← G.map_comp, ← f.h, comparison_obj_A, comparison_obj_a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ (G ⋙ F).map f.f) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
have rw : adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ F.map (G.map f.f)) =
  adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
Tactic: rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
rw :
  adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ (G ⋙ F).map f.f) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
have rw₁ : adj.unit.app B ≫ G.map (F.map (adj.unit.app B)) ≫ G.map (F.map (G.map f.f)) =
  adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
Tactic: rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
rw :
  adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
rw₁ :
  adj.unit.app B ≫ G.map (F.map (adj.unit.app B)) ≫ G.map (F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ (G ⋙ F).map f.f) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
have rw₂ : adj.unit.app B ≫ adj.unit.app (G.obj (F.obj B)) ≫ G.map (F.map (G.map f.f)) =
  adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
Tactic: rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality]