mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapₗ F =
    LaxMonoidal.ofBifunctor.topMapₗ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      (curriedTensorPreIsoPost L W F G).hom.app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapₗ F

pp: case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapᵣ F =
    LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapᵣ F

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapₗ F =
    LaxMonoidal.ofBifunctor.topMapₗ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      (curriedTensorPreIsoPost L W F G).hom.app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapₗ F
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapᵣ F =
    LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapᵣ F

Tactic:
·

Goal state after:
case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapᵣ F =
    LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapᵣ F
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
⊢ ε (L ⋙ F) ≫ (Lifting.iso L W G F).hom.app (𝟙_ C) = ε G

pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
x✝¹ x✝ : C
⊢ μ (L ⋙ F) x✝¹ x✝ ≫ (Lifting.iso L W G F).hom.app (x✝¹ ⊗ x✝) =
    ((Lifting.iso L W G F).hom.app x✝¹ ⊗ₘ (Lifting.iso L W G F).hom.app x✝) ≫ μ G x✝¹ x✝

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
⊢ ε (L ⋙ F) ≫ (Lifting.iso L W G F).hom.app (𝟙_ C) = ε G
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
x✝¹ x✝ : C
⊢ μ (L ⋙ F) x✝¹ x✝ ≫ (Lifting.iso L W G F).hom.app (x✝¹ ⊗ x✝) =
    ((Lifting.iso L W G F).hom.app x✝¹ ⊗ₘ (Lifting.iso L W G F).hom.app x✝) ≫ μ G x✝¹ x✝

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
x✝¹ x✝ : C
⊢ μ (L ⋙ F) x✝¹ x✝ ≫ (Lifting.iso L W G F).hom.app (x✝¹ ⊗ x✝) =
    ((Lifting.iso L W G F).hom.app x✝¹ ⊗ₘ (Lifting.iso L W G F).hom.app x✝) ≫ μ G x✝¹ x✝
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ ≫
      ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom) =
    (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g) ≫
      ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom)

pp: case h₂
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom) =
    (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g) ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom)

Tactic:
·

Goal state after:
case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ ≫
      ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom) =
    (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g) ≫
      ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: case h₂
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom) =
    (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g) ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom)

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom) =
    (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g) ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
a : T✝ ⟶ Y
b : T✝ ⟶ Z
m : T✝ ⟶ (binaryFan Y Z).pt
h₁ : m ≫ (binaryFan Y Z).fst = a
h₂ : m ≫ (binaryFan Y Z).snd = b
⊢ m = Over.homMk (lift (Over.Hom.left a) (Over.Hom.left b) ⋯) ⋯

Tactic:
by
      ext
      dsimp [Over.map, Comma.mapRight]
      cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj ((𝟭 C).obj A.A))

pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))

Tactic:
·

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj ((𝟭 C).obj A.A))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))

Tactic:
·

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B : D
⊢ (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)

pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ ∀ (X : adj.toMonad.Algebra) (Y Y' : D) (g : Y ⟶ Y') (h : comparisonLeftAdjointObj adj X ⟶ Y),
    ?refine_1 (h ≫ g) = ?refine_1 h ≫ (comparison adj).map g

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B : D
⊢ (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ ∀ (X : adj.toMonad.Algebra) (Y Y' : D) (g : Y ⟶ Y') (h : comparisonLeftAdjointObj adj X ⟶ Y),
    (comparisonLeftAdjointHomEquiv adj X Y') (h ≫ g) =
      (comparisonLeftAdjointHomEquiv adj X Y) h ≫ (comparison adj).map g

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ ∀ (X : adj.toMonad.Algebra) (Y Y' : D) (g : Y ⟶ Y') (h : comparisonLeftAdjointObj adj X ⟶ Y),
    (comparisonLeftAdjointHomEquiv adj X Y') (h ≫ g) =
      (comparisonLeftAdjointHomEquiv adj X Y) h ≫ (comparison adj).map g
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
inst✝ : HasCoequalizer (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]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))

Tactic:
·

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    ((colimit.isColimit
            (parallelPair (F.map (G.map (adj.counit.app Y)))
              (adj.counit.app (F.obj (G.obj Y))))).coconePointUniqueUpToIso
        ?m.215).hom

pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsColimit (counitCofork adj Y)

Tactic:
·

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    ((colimit.isColimit
            (parallelPair (F.map (G.map (adj.counit.app Y)))
              (adj.counit.app (F.obj (G.obj Y))))).coconePointUniqueUpToIso
        ?m.215).hom
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))

Tactic:
·

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    ((colimit.isColimit
            (parallelPair (F.map (G.map (adj.counit.app Y)))
              (adj.counit.app (F.obj (G.obj Y))))).coconePointUniqueUpToIso
        ?m.194).hom

pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsColimit (counitCofork adj Y)

Tactic:
·

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    ((colimit.isColimit
            (parallelPair (F.map (G.map (adj.counit.app Y)))
              (adj.counit.app (F.obj (G.obj Y))))).coconePointUniqueUpToIso
        ?m.194).hom
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
⊢ (comparison adj).IsEquivalence

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]
        exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
          (unitColimitOfPreservesCoequalizer X)).isIso_hom
    have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) := by
      intro Y
      rw [comparisonAdjunction_counit_app]
      -- Porting note: passing instances through
      change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
      · infer_instance
      -- Porting note: passing instances through
      apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_
      apply reflectsColimit_of_reflectsIsomorphisms
    exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
⊢ (F.map (λ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F (𝟙_ C) c).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.εIso F).unmop.app ((F.obj c).unmop.obj d)).symm.hom

Tactic:
have e := (F.map (λ_ c).hom).unmop.app d ≫=
      (congrArg (fun t ↦ t.unmop.app d) <|
        Functor.OplaxMonoidal.left_unitality F c)
    dsimp at e
    simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp,
      ← F.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, Category.id_comp] at e
    simp [e]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) =
    (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) =
    (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
·

Goal state after:
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) =
    (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))