mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
i : ℕ
hi : i < n + 1
⊢ (δ₀Functor.map (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w)).app ⟨i, hi⟩ = (δ₀Functor.map (𝟙 G)).app ⟨i, hi⟩

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ i < n + 1

Tactic:
valid

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ F.obj ⟨i + 1, hi⟩ = G.obj ⟨i + 1, hi⟩

Tactic:
exact Functor.congr_obj h ⟨i, by valid⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), (liftedCocone c t).ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J✝), c.ι.app j ≫ m.f = c.ι.app j ≫ { f := t.desc (T.forget.mapCocone s), h := ⋯ }.f

Tactic:
intro j

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), (liftedCocone c t).ι.app j ≫ m = s.ι.app j
j : J✝
⊢ c.ι.app j ≫ m.f = c.ι.app j ≫ { f := t.desc (T.forget.mapCocone s), h := ⋯ }.f
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
hi : 0 < n + 1 + 1
⊢ (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app ⟨0, hi⟩ = eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
⊢ (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app ⟨n✝ + 1, hi⟩ = eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C (n + 1)
⊢ F.δ₀ = (F.δ₀.precomp (F.map' 0 1 ⋯ ⋯)).δ₀

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C (n + 1)
⊢ F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom ⋯ ≫ (F.δ₀.precomp (F.map' 0 1 ⋯ ⋯)).map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
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₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_246 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_246) _auto_266
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_247 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_247) _auto_268
⊢ 2 < 2 + 1

Tactic:
valid

Goal state after:
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:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 2
⊢ X.map' 0 1 homMk₁._proof_4 _proof_246 =
    eqToHom ⋯ ≫ (mk₂ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯)).map' 0 1 homMk₁._proof_4 _proof_246 ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 2
⊢ X.map' 1 2 _proof_246 _proof_247 =
    eqToHom ⋯ ≫ (mk₂ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯)).map' 1 2 _proof_246 _proof_247 ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
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₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_298 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_298) _auto_318
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_299 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_299) _auto_320
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_300 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_300) _auto_322
⊢ 2 < 3 + 1

Tactic:
valid

Goal state after:
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₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_298 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_298) _auto_325
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_299 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_299) _auto_327
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_300 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_300) _auto_329
⊢ 3 < 3 + 1

Tactic:
valid

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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
m : (liftedCocone D c t).pt ⟶ s.pt
J : ∀ (j : J✝), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J✝), c.ι.app j ≫ m.f = c.ι.app j ≫ { f := t.desc (T.forget.mapCocone s), h := ⋯ }.f

Tactic:
intro j

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
m : (liftedCocone D c t).pt ⟶ s.pt
J : ∀ (j : J✝), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j
j : J✝
⊢ c.ι.app j ≫ m.f = c.ι.app j ≫ { f := t.desc (T.forget.mapCocone s), h := ⋯ }.f
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 3
⊢ X.map' 0 1 homMk₁._proof_4 _proof_298 =
    eqToHom ⋯ ≫ (mk₃ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯)).map' 0 1 homMk₁._proof_4 _proof_298 ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 3
⊢ X.map' 1 2 _proof_246 _proof_299 =
    eqToHom ⋯ ≫ (mk₃ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯)).map' 1 2 _proof_246 _proof_299 ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 3
⊢ X.map' 2 3 _proof_299 _proof_300 =
    eqToHom ⋯ ≫ (mk₃ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯)).map' 2 3 _proof_299 _proof_300 ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
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 4
app₀ : f.obj' 0 _proof_361 ⟶ g.obj' 0 _proof_361
app₁ : f.obj' 1 _proof_362 ⟶ g.obj' 1 _proof_362
app₂ : f.obj' 2 _proof_363 ⟶ g.obj' 2 _proof_363
app₃ : f.obj' 3 _proof_364 ⟶ g.obj' 3 _proof_364
app₄ : f.obj' 4 _proof_365 ⟶ g.obj' 4 _proof_365
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_362 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_362) _auto_387
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_363 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_363) _auto_389
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_364 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_364) _auto_391
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_365 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_365) _auto_393
⊢ 2 < 4 + 1

Tactic:
valid

Goal state after:
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 4
app₀ : f.obj' 0 _proof_361 ⟶ g.obj' 0 _proof_361
app₁ : f.obj' 1 _proof_362 ⟶ g.obj' 1 _proof_362
app₂ : f.obj' 2 _proof_363 ⟶ g.obj' 2 _proof_363
app₃ : f.obj' 3 _proof_364 ⟶ g.obj' 3 _proof_364
app₄ : f.obj' 4 _proof_365 ⟶ g.obj' 4 _proof_365
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_362 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_362) _auto_396
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_363 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_363) _auto_398
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_364 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_364) _auto_400
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_365 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_365) _auto_402
⊢ 3 < 4 + 1

Tactic:
valid

Goal state after:
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 4
app₀ : f.obj' 0 _proof_361 ⟶ g.obj' 0 _proof_361
app₁ : f.obj' 1 _proof_362 ⟶ g.obj' 1 _proof_362
app₂ : f.obj' 2 _proof_363 ⟶ g.obj' 2 _proof_363
app₃ : f.obj' 3 _proof_364 ⟶ g.obj' 3 _proof_364
app₄ : f.obj' 4 _proof_365 ⟶ g.obj' 4 _proof_365
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_362 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_362) _auto_405
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_363 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_363) _auto_407
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_364 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_364) _auto_409
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_365 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_365) _auto_411
⊢ 4 < 4 + 1

Tactic:
valid

Goal state after:
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 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 0 + 1 ≤ 4

Tactic:
valid

Goal state after:
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 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 1 + 1 ≤ 4

Tactic:
valid

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
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J✝), m ≫ (liftedCone c t).π.app j = s.π.app j
⊢ ∀ (j : J✝), m.f ≫ c.π.app j = { f := t.lift (T.forget.mapCone s), h := ⋯ }.f ≫ c.π.app j

Tactic:
intro j

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
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J✝), m ≫ (liftedCone c t).π.app j = s.π.app j
j : J✝
⊢ m.f ≫ c.π.app j = { f := t.lift (T.forget.mapCone s), h := ⋯ }.f ≫ 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 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 2 + 1 ≤ 4

Tactic:
valid

Goal state after:
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 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 3 + 1 ≤ 4

Tactic:
valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 4
⊢ X.map' 0 1 homMk₁._proof_4 _proof_362 =
    eqToHom ⋯ ≫
      (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 0 1 homMk₁._proof_4 _proof_362 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 4
⊢ X.map' 1 2 _proof_246 _proof_363 =
    eqToHom ⋯ ≫
      (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 1 2 _proof_246 _proof_363 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 4
⊢ X.map' 2 3 _proof_299 _proof_364 =
    eqToHom ⋯ ≫
      (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 2 3 _proof_299 _proof_364 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 4
⊢ X.map' 3 4 _proof_364 _proof_365 =
    eqToHom ⋯ ≫
      (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 3 4 _proof_364 _proof_365 ≫
        eqToHom ⋯

Tactic:
simp

Goal state after:
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 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_480
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_482
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_484
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_486
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_488
⊢ 2 < 5 + 1

Tactic:
valid

Goal state after:
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 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_491
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_493
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_495
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_497
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_499
⊢ 3 < 5 + 1

Tactic:
valid

Goal state after:
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 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_502
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_504
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_506
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_508
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_510
⊢ 4 < 5 + 1

Tactic:
valid

Goal state after:
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 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_513
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_515
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_517
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_519
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_521
⊢ 5 < 5 + 1

Tactic:
valid

Goal state after:
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 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 0 + 1 ≤ 5

Tactic:
valid

Goal state after: