mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y))
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ G.map (F.map (adj.unit.app Y) ≫ adj.counit.app (F.1 ((𝟭 C).obj Y))) = G.map (𝟙 ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ G.map (F.map (adj.unit.app Y) ≫ adj.counit.app (F.1 ((𝟭 C).obj Y))) = G.map (𝟙 ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    G.map (𝟙 ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    G.map (𝟙 ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_246✝ = f.map' 0 1 homMk₁._proof_4 _proof_246✝

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).f) ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).g)

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).f) ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).g)
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorRight M)).f) ⇑(ConcreteCategory.hom (C.map (tensorRight M)).g)

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorRight M)).f) ⇑(ConcreteCategory.hom (C.map (tensorRight M)).g)
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ PreservesFiniteLimits (tensorLeft M) ∧ PreservesFiniteColimits (tensorLeft M) ↔ PreservesFiniteLimits (tensorLeft M)

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ PreservesFiniteLimits (tensorLeft M) ∧ PreservesFiniteColimits (tensorLeft M) ↔ PreservesFiniteLimits (tensorLeft M)
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
⊢ Flat R ↑M

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
⊢ Flat R ↑M
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
x✝ : PreservesFiniteLimits (tensorRight M)
⊢ PreservesFiniteLimits (tensorLeft M)

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x✝ : PreservesFiniteLimits (tensorRight M)
⊢ PreservesFiniteLimits (tensorLeft M)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 1 2 _proof_246✝ _proof_247✝ = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_247✝

Tactic:
app₁.hom_inv_id_assoc

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 1 2 _proof_246✝ _proof_247✝ = f.map' 1 2 _proof_246✝ _proof_247✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 1 2 _proof_246✝ _proof_247✝ = f.map' 1 2 _proof_246✝ _proof_247✝

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
⊢ (∀ (X : Fin (2 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
⊢ (∀ (X : Fin (2 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : Flat R S
inst✝ : Flat S M
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(LinearMap.lTensor M N.subtype)

Tactic:
]

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : Flat R S
inst✝ : Flat S M
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(LinearMap.lTensor M N.subtype)
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype))

Tactic:
]

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype))
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : CommSemiring Rp
inst✝⁵ : Algebra R Rp
inst✝⁴ : AddCommMonoid Mp
inst✝³ : Module R Mp
inst✝² : Module Rp Mp
inst✝¹ : IsScalarTower R Rp Mp
inst✝ : Flat R M
S : Submonoid R
⊢ IsLocalizedModule S (LocalizedModule.mkLinearMap S M)

Tactic:
]

Goal state after:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : CommSemiring Rp
inst✝⁵ : Algebra R Rp
inst✝⁴ : AddCommMonoid Mp
inst✝³ : Module R Mp
inst✝² : Module Rp Mp
inst✝¹ : IsScalarTower R Rp Mp
inst✝ : Flat R M
S : Submonoid R
⊢ IsLocalizedModule S (LocalizedModule.mkLinearMap S M)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ c.ι.app j = c.ι.app j

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
g : x₀ ⟶ x₁
g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_246 _proof_247)
⊢ Arrow.mk f = Arrow.mk g

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
g : x₀ ⟶ x₁
g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_246 _proof_247)
⊢ Arrow.mk f = Arrow.mk g
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j))

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_246 _proof_247)
⊢ Arrow.mk f' = Arrow.mk g'

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_246 _proof_247)
⊢ Arrow.mk f' = Arrow.mk g'
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (D.obj j).a ≫ T.map ((T.forget.mapCocone s).ι.app j) = T.forget.map (s.ι.app j) ≫ s.pt.a

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (D.obj j).a ≫ T.map ((T.forget.mapCocone s).ι.app j) = T.forget.map (s.ι.app j) ≫ s.pt.a
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_298✝ = f.map' 0 1 homMk₁._proof_4 _proof_298✝

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 1 2 _proof_246✝ _proof_299✝ = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_299✝

Tactic:
app₁.hom_inv_id_assoc

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 1 2 _proof_246✝ _proof_299✝ = f.map' 1 2 _proof_246✝ _proof_299✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 1 2 _proof_246✝ _proof_299✝ = f.map' 1 2 _proof_246✝ _proof_299✝

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 2 3 _proof_299✝ _proof_300✝ = f.map' 2 3 _proof_299✝ _proof_300✝

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ c.π.app ?m.162 ≫ (D ⋙ T.forget).map ?m.164 = c.π.app A ≫ (D.map f).f

pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ ?m.162 ⟶ B

pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ J

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ c.π.app ?m.162 ≫ (D ⋙ T.forget).map ?m.164 = c.π.app A ≫ (D.map f).f

C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ ?m.162 ⟶ B

C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ J
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
⊢ f.map' n (n + 1) ⋯ h = f.map' n (n + 1) ⋯ h

Tactic:
]

Goal state after: