[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
[PROOFSTEP]
apply IsReflexivePair.mk' _ _ _
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ (free T).obj X.A ⟶ (free T).obj (T.obj X.A)
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ?m.2463 ≫ FreeCoequalizer.topMap X = 𝟙 ((free T).obj X.A)
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ?m.2463 ≫ FreeCoequalizer.bottomMap X = 𝟙 ((free T).obj X.A)
[PROOFSTEP]
apply (free T).map (T.η.app X.A)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ (free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.topMap X = 𝟙 ((free T).obj X.A)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ((free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.topMap X).f = (𝟙 ((free T).obj X.A)).f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ T.map (NatTrans.app (η T) X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)
[PROOFSTEP]
rw [← Functor.map_comp, X.unit, Functor.map_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ (free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 ((free T).obj X.A)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ((free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.bottomMap X).f = (𝟙 ((free T).obj X.A)).f
[PROOFSTEP]
apply Monad.right_unit
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
⊢ { l //
    Cofork.π (beckAlgebraCofork X) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
have h₁ : (T : C ⥤ C).map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f := congr_arg Monad.Algebra.Hom.f s.condition
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ { l //
    Cofork.π (beckAlgebraCofork X) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
have h₂ : (T : C ⥤ C).map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f := s.π.h
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ { l //
    Cofork.π (beckAlgebraCofork X) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
refine' ⟨⟨T.η.app _ ≫ s.π.f, _⟩, _, _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ T.map (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ T.map (NatTrans.app (η T) X.1 ≫ (Cofork.π s).f) ≫ s.pt.a = X.a ≫ NatTrans.app (η T) X.1 ≫ (Cofork.π s).f
[PROOFSTEP]
rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc, show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _,
  h₁, Monad.left_unit_assoc]
[GOAL]
case refine'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ Cofork.π (beckAlgebraCofork X) ≫ Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f) =
    Cofork.π s
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ (Cofork.π (beckAlgebraCofork X) ≫ Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)).f =
    (Cofork.π s).f
[PROOFSTEP]
simpa [← T.η.naturality_assoc, T.left_unit_assoc] using T.η.app ((T : C ⥤ C).obj X.A) ≫= h₁
[GOAL]
case refine'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
    Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s →
      m = Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m = Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)
[PROOFSTEP]
ext
[GOAL]
case refine'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m.f = (Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)).f
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m.f = NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f
[PROOFSTEP]
rw [← hm]
[GOAL]
case refine'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m.f = NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π (beckAlgebraCofork X) ≫ m).f
[PROOFSTEP]
apply (X.unit_assoc _).symm
