mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
⊢ g.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_298✝

Tactic:
by

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
⊢ m = { f := t.desc (T.forget.mapCocone s), h := ⋯ }

Tactic:
by

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
⊢ (lambda c t ≫ T.ε.app c.pt) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
by

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₀ : 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✝
⊢ g.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_299✝

Tactic:
by

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
⊢ lambda c t ≫ T.δ.app c.pt = lambda c t ≫ T.map (lambda c t)

Tactic:
by

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₀ : 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✝
⊢ g.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_299✝ _proof_300✝

Tactic:
by

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' 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:
by

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:
by

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:
by

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:
by

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:
by

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
⊢ ((const J).obj (conePoint c t)).map f ≫ { f := c.π.app B, h := ⋯ } = { f := c.π.app A, h := ⋯ } ≫ D.map f

Tactic:
by

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:
by

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 : ℕ
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
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ ∀ {X Y Z : WalkingReflexivePair} (f_1 : X ⟶ Y) (g_1 : Y ⟶ Z),
    (match X, Z, f_1 ≫ g_1 with
      | x, .(x), Hom.id .(x) =>
        𝟙
          (match x with
          | zero => B
          | one => A)
      | .(one), .(zero), Hom.left => f
      | .(one), .(zero), Hom.right => g
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
      (match X, Y, f_1 with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s) ≫
        match Y, Z, g_1 with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s

Tactic:
by

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✝
⊢ g.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_362✝

Tactic:
by

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
j : J
⊢ (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ (T.mapCone c).π.app j =
    (t.lift (T.forget.mapCone s) ≫ (liftedCone c t).pt.a) ≫ (T.mapCone c).π.app j

Tactic:
by

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:
by

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✝
⊢ g.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_363✝

Tactic:
by

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✝
⊢ 2 + 1 ≤ 4

Tactic:
by

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
⊢ m = { f := t.lift (T.forget.mapCone s), h := ⋯ }

Tactic:
by

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
inst✝¹ : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cone (D ⋙ T.forget)
t : IsLimit c
A B : J
f : A ⟶ B
⊢ ((const J).obj (conePoint c t)).map f ≫ { f := c.π.app B, h := ⋯ } = { f := c.π.app A, h := ⋯ } ≫ D.map f

Tactic:
by

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
inst✝ : PreservesLimitsOfShape J T.toFunctor
⊢ {K : J ⥤ T.Coalgebra} → CreatesLimit K T.forget

Tactic:
by

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
inst✝ : PreservesLimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor
⊢ {J : Type u} → [inst : Category.{v, u} J] → CreatesLimitsOfShape J T.forget

Tactic:
by

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✝
⊢ g.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_299✝ _proof_364✝

Tactic:
by

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
F : J ⥤ D
R : D ⥤ C
inst✝¹ : ComonadicLeftAdjoint R
inst✝ : HasColimit (F ⋙ R)
⊢ HasColimit ((F ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ (comonadicAdjunction R).toComonad.forget)

Tactic:
by

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:
by

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
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ (comonadicAdjunction R).toComonad.forget ≅ K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R)) (comonadicAdjunction R).toComonad.forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
⊢ PreservesLimit ((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) (comonadicAdjunction R).toComonad.toFunctor

Tactic:
by

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
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ (comonadicAdjunction R).toComonad.forget ≅ K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R)) (comonadicAdjunction R).toComonad.forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
this : PreservesLimit ((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget)
  (comonadicAdjunction R).toComonad.toFunctor :=
  comonadicCreatesLimitOfPreservesLimit._proof_1 R K
⊢ PreservesLimit (((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) ⋙ (comonadicAdjunction R).toComonad.toFunctor)
    (comonadicAdjunction R).toComonad.toFunctor

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
x✝¹ x✝ : WalkingReflexivePair
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫
      match x✝ with
      | zero => e₀
      | one => e₁) =
    (match x✝¹ with
      | zero => e₀
      | one => e₁) ≫
      G.map f

Tactic:
by

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✝
⊢ g.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_364✝ _proof_365✝

Tactic:
by

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:
by

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:
by

Goal state after: