awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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.{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:
simp [Cofork.IsColimit.homIso, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Limits.Cofork.IsColimit.homIso
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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))
    ((adj.homEquiv A.A (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))) :
        (a : F.obj A.A ⟶ coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))) →
          A.A ⟶ G.obj (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
      (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))))

Tactic:
congr_arg (adj.homEquiv _ _) (Category.comp_id _)

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.colimit, congr_arg, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj, CategoryTheory.Adjunction.homEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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))))
rw₂ 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))))
⊢ 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))))

Tactic:
rw [← G.map_comp, coequalizer.condition, G.map_comp]

Premises used: CategoryTheory.Limits.coequalizer.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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))
⊢ (unitCofork A).π = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
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))
⊢ 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))

Tactic:
apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A)

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.Monad.beckCoequalizer
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
rw : (beckCofork A).π ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A) = (unitCofork A).π
⊢ 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:
rw [Cofork.IsColimit.π_desc]

Premises used: CategoryTheory.Limits.Cofork.IsColimit.π_desc
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
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))))
⊢ (beckCofork A).π ≫ Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) A) = (unitCofork A).π

Tactic:
dsimp only [beckCofork_π, unitCofork_π]

Premises used: CategoryTheory.Monad.MonadicityInternal.unitCofork_π, CategoryTheory.Monad.beckCofork_π
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
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))))
⊢ 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:
rw [comparisonAdjunction_unit_f_aux, ← adj.homEquiv_naturality_left A.a, coequalizer.condition,
    adj.homEquiv_naturality_right, adj.homEquiv_unit, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Monad.Algebra.a, CategoryTheory.Limits.coequalizer.condition, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, CategoryTheory.Adjunction.homEquiv_naturality_right, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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)
    (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:
apply adj.right_triangle_components_assoc

Premises used: CategoryTheory.Adjunction.right_triangle_components_assoc
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
⊢ HasColimit (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))

Tactic:
inferInstanceAs <| HasCoequalizer
    (F.map ((comparison adj).obj B).a)
    (adj.counit.app (F.obj ((comparison adj).obj B).A))

Premises used: _private.0.CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA._proof_1
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
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))
⊢ 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))

Tactic:
apply coequalizer.hom_ext

Premises used: CategoryTheory.Limits.coequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
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))) ⋯) =
    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) ⋯)
⊢ 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:
change
    coequalizer.π _ _ ≫ coequalizer.desc ((adj.homEquiv _ B).symm (𝟙 _)) _ =
      coequalizer.π _ _ ≫ coequalizer.desc _ _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.coequalizer.desc, CategoryTheory.Adjunction.homEquiv, Equiv.symm, CategoryTheory.Limits.coequalizer.π, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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)))
      (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))) ⋯) =
    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) ⋯)

Tactic:
simp [Adjunction.homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_counit
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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)
inst₁ : PreservesColimit ((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G) (monadicLeftAdjoint G ⋙ G)
⊢ CreatesColimit (parallelPair f g) G

Tactic:
apply +allowSynthFailures monadicCreatesColimitOfPreservesColimit

Premises used: CategoryTheory.monadicCreatesColimitOfPreservesColimit
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
apply :
  PreservesColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)
⊢ PreservesColimit (parallelPair f g ⋙ G) (monadicLeftAdjoint G ⋙ G)

Tactic:
apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
dsimp : PreservesColimit (parallelPair (G.map f) (G.map g)) (monadicLeftAdjoint G ⋙ G)
⊢ PreservesColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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 (G.map f) (G.map g)) (monadicLeftAdjoint G ⋙ G)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
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)
⊢ PreservesColimit ((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G) (monadicLeftAdjoint G ⋙ G)

Tactic:
apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
dsimp :
  PreservesColimit
    (parallelPair (G.map ((monadicLeftAdjoint G).map (G.map f))) (G.map ((monadicLeftAdjoint G).map (G.map g))))
    (monadicLeftAdjoint G ⋙ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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 (G.map ((monadicLeftAdjoint G).map (G.map f))) (G.map ((monadicLeftAdjoint G).map (G.map g))))
    (monadicLeftAdjoint G ⋙ G)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
⊢ ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))

Tactic:
fun _ => HasCoequalizerOfIsSplitPair.out G _ _

Premises used: CategoryTheory.Monad.HasCoequalizerOfIsSplitPair.out, CategoryTheory.Monad.Algebra.a, CategoryTheory.Monad.Algebra.A, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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 B : D
f g : A ⟶ B
inst_2 : G.IsSplitPair f g
inst_3 : PreservesColimitOfIsSplitPair G
⊢ PreservesColimit (parallelPair f g) G

Tactic:
PreservesColimitOfIsSplitPair.out f g

Premises used: CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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 : PreservesColimitOfIsSplitPair G
⊢ ∀ (A : adj.toMonad.Algebra), PreservesColimit (parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G

Tactic:
fun _ => PreservesColimitOfIsSplitPair.out _ _

Premises used: CategoryTheory.Monad.Algebra.a, CategoryTheory.Monad.Algebra.A, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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 B : D
f g : A ⟶ B
inst_2 : G.IsSplitPair f g
inst_3 : ReflectsColimitOfIsSplitPair G
⊢ ReflectsColimit (parallelPair f g) G

Tactic:
ReflectsColimitOfIsSplitPair.out f g

Premises used: CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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 : ReflectsColimitOfIsSplitPair G
⊢ ∀ (A : adj.toMonad.Algebra), ReflectsColimit (parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G

Tactic:
fun _ => ReflectsColimitOfIsSplitPair.out _ _

Premises used: CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out, CategoryTheory.Monad.Algebra.a, CategoryTheory.Monad.Algebra.A, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
apply :
  IsIso (Y := adj.toMonad.forget.obj ((leftAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toMonad.forget.map (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
⊢ IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
    (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)

Tactic:
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _

Premises used: CategoryTheory.Monad.forget, CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Adjunction.toMonad
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
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
change :
  IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
⊢ IsIso (Y := adj.toMonad.forget.obj ((leftAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toMonad.forget.map (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))

Tactic:
change IsIso ((comparisonAdjunction adj).unit.app X).f

Premises used: CategoryTheory.IsIso, CategoryTheory.Adjunction.unit, CategoryTheory.Monad.Algebra.Hom.f, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction, CategoryTheory.NatTrans.app