awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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)
⊢ adj.toMonad.Algebra ⥤ D
have 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')
Tactic: refine
    Adjunction.leftAdjointOfEquiv (G := comparison adj)
      (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
⊢ 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')
have 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))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (F.map A.a) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
have rw : Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
  (G.map (F.map A.a ≫ coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
  (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
Tactic: rw [← G.map_comp, coequalizer.condition, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
rw :
  Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (F.map A.a ≫ coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
⊢ Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (F.map A.a) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
have rw₁ : Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
  (G.map (adj.counit.app (F.obj A.A) ≫ coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
  (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
Tactic: rw [← G.map_comp, coequalizer.condition, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
rw :
  Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (F.map A.a ≫ coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
rw₁ :
  Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (adj.counit.app (F.obj A.A) ≫ coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
⊢ Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (F.map A.a) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
    (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
have rw₂ : Eq (α := G.obj (F.obj (adj.toMonad.obj A.A)) ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
  (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
  (G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
Tactic: rw [← G.map_comp, coequalizer.condition, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
⊢ Eq (α := (Functor.obj (𝟭 adj.toMonad.Algebra) A).A ⟶ ((leftAdjointComparison adj ⋙ comparison adj).obj A).A)
    (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A))
    ((beckCoequalizer A).desc (unitCofork A))
have apply : Eq (α := adj.toMonad.obj A.A ⟶ ((leftAdjointComparison adj ⋙ comparison adj).obj A).A)
  ((beckCofork A).π ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A))
  ((beckCofork A).π ≫ (beckCoequalizer A).desc (unitCofork A))
Tactic: apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
⊢ Eq (α := adj.toMonad.obj A.A ⟶ ((leftAdjointComparison adj ⋙ comparison adj).obj A).A)
    ((beckCofork A).π ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A))
    ((beckCofork A).π ≫ (beckCoequalizer A).desc (unitCofork A))
have rw : (beckCofork A).π ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A) = (unitCofork A).π
Tactic: rw [Cofork.IsColimit.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
⊢ (beckCofork A).π ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A) = (unitCofork A).π
have dsimp : Eq (α := adj.toMonad.obj A.A ⟶ ((leftAdjointComparison adj ⋙ comparison adj).obj A).A)
  (A.a ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A))
  (G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
Tactic: dsimp only [beckCofork_π, unitCofork_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
⊢ Eq (α := adj.toMonad.obj A.A ⟶ ((leftAdjointComparison adj ⋙ comparison adj).obj A).A)
    (A.a ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A))
    (G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
have rw : Eq (α := adj.toMonad.obj A.A ⟶ ((leftAdjointComparison adj ⋙ comparison adj).obj A).A)
  (adj.unit.app (adj.toMonad.obj A.A) ≫
    G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
  (G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))
Tactic: rw [comparisonAdjunction_unit_f_aux, ← adj.homEquiv_naturality_left A.a, coequalizer.condition,
    adj.homEquiv_naturality_right, adj.homEquiv_unit, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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))
B : D
⊢ Eq (α := (comparison adj ⋙ leftAdjointComparison adj).obj B ⟶ Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) B)
    (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) B)
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
      (counitCofork adj B))
have h : CategoryStruct.comp (Y :=
    coequalizer (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) B) =
  CategoryStruct.comp (Y :=
    coequalizer (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
      (counitCofork adj B))
Tactic: apply coequalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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))
B : D
⊢ CategoryStruct.comp (Y :=
      coequalizer (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
      (coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
      (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) B) =
    CategoryStruct.comp (Y :=
      coequalizer (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
      (coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
      (colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
        (counitCofork adj B))
have h : CategoryStruct.comp (Y :=
    coequalizer (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (coequalizer.desc
      ((Equiv.symm (adj.homEquiv (G.obj B) B) : (a : G.obj B ⟶ G.obj B) → F.obj (G.obj B) ⟶ B) (𝟙 (G.obj B))) sorry) =
  CategoryStruct.comp (Y :=
    coequalizer (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)))
    (coequalizer.desc (adj.counit.app B) sorry)
Tactic: change
    coequalizer.π _ _ ≫ coequalizer.desc ((adj.homEquiv _ B).symm (𝟙 _)) _ =
      coequalizer.π _ _ ≫ coequalizer.desc _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ CreatesColimit (parallelPair f g) G
have inst : PreservesColimit (parallelPair f g ⋙ G) (monadicLeftAdjoint G ⋙ G)
Tactic: apply +allowSynthFailures monadicCreatesColimitOfPreservesColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_3 : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst_4 : G.IsSplitPair f g
inst : PreservesColimit (parallelPair f g ⋙ G) (monadicLeftAdjoint G ⋙ G)
⊢ CreatesColimit (parallelPair f g) G
have inst₁ : PreservesColimit ((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G) (monadicLeftAdjoint G ⋙ G)
Tactic: apply +allowSynthFailures monadicCreatesColimitOfPreservesColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ PreservesColimit (parallelPair f g ⋙ G) (monadicLeftAdjoint G ⋙ G)
have apply : PreservesColimit
  (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
    ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
  (monadicLeftAdjoint G ⋙ G)
Tactic: apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ PreservesColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)
have dsimp : PreservesColimit (parallelPair (G.map f) (G.map g)) (monadicLeftAdjoint G ⋙ G)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ PreservesColimit ((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G) (monadicLeftAdjoint G ⋙ G)
have apply : PreservesColimit
  (parallelPair (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.left)
    (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.right))
  (monadicLeftAdjoint G ⋙ G)
Tactic: apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ PreservesColimit
    (parallelPair (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.left)
      (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)
have dsimp : PreservesColimit
  (parallelPair (G.map ((monadicLeftAdjoint G).map (G.map f))) (G.map ((monadicLeftAdjoint G).map (G.map g))))
  (monadicLeftAdjoint G ⋙ G)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
    (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
have apply : IsIso (Y := adj.toMonad.forget.obj ((leftAdjointComparison adj ⋙ comparison adj).obj X))
  (adj.toMonad.forget.map (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
Tactic: apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := adj.toMonad.forget.obj ((leftAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toMonad.forget.map (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
have change : IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
  (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
Tactic: change IsIso ((comparisonAdjunction adj).unit.app X).f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
have rw : IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
  ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)
Tactic: rw [comparisonAdjunction_unit_f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)
have this : IsIso (Y := (unitCofork X).pt)
  (Iso.hom ((beckCoequalizer X).coconePointUniqueUpToIso (unitColimitOfPreservesCoequalizer X)))
Tactic: change
          IsIso
            (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
                (unitColimitOfPreservesCoequalizer X)).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
⊢ (comparison adj).IsEquivalence
have this : ∀ (X : adj.toMonad.Algebra),
  IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
    (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Tactic: have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by
      intro X
      apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).unit.app X).f
        rw [comparisonAdjunction_unit_f]
        change
          IsIso
            (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
                (unitColimitOfPreservesCoequalizer X)).hom
        exact (IsColimit.coconePointUniqueUpToIso _ _).isIso_hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Y : D
⊢ IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y)
    (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) Y)
have rw : IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y) (Y := Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) Y)
  (colimit.desc (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))
      (counitCofork adj Y) :
    colimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) ⟶
      (counitCofork adj Y).pt)
Tactic: rw [comparisonAdjunction_counit_app]