mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair),
    (Multicofork.toSigmaCofork hc hd K₁).ι.app j ≫ f.hom = (Multicofork.toSigmaCofork hc hd K₂).ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ (coreflectorAdjunction R).counit.app X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingMultispan J), (Multicofork.ofSigmaCofork K₁).ι.app j ≫ f.hom = (Multicofork.ofSigmaCofork K₂).ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K : Multicofork I
⊢ ∀ (j : WalkingMultispan J),
    ((𝟭 (Multicofork I)).obj K).ι.app j ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
      ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
⊢ ((I.ofSigmaCoforkFunctor hc ⋙ I.toSigmaCoforkFunctor hc hd).obj K).π ≫
      (Iso.refl ((I.ofSigmaCoforkFunctor hc ⋙ I.toSigmaCoforkFunctor hc hd).obj K).pt).hom =
    ((𝟭 (Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))).obj K).π

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
⊢ (Comonad.comparison (coreflectorAdjunction R)).EssSurj

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ ιPi I ≫ Pi.π I.left a = ι I a

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : R.Full
L : C ⥤ D
adj : R ⊣ L
X✝ Y✝ : D
f : (Comonad.comparison adj).obj X✝ ⟶ (Comonad.comparison adj).obj Y✝
⊢ (Comonad.comparison adj).map (R.preimage f.f) = 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 : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i j k : Fin (n + 1 + 1)
hij : i ≤ j
hjk : j ≤ k
⊢ map F f i k ⋯ = map F f i j hij ≫ map F f j k hjk

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 : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i j k : Fin (n + 1 + 1)
hij : i ≤ j
hjk : j ≤ k
⊢ map F f i k ⋯ = map F f i j hij ≫ map F f j k hjk

Tactic:
by
  obtain ⟨i, hi⟩ := i
  obtain ⟨j, hj⟩ := j
  obtain ⟨k, hk⟩ := k
  cases i
  · obtain _ | _ | j := j
    · dsimp
      rw [id_comp]
    · obtain _ | _ | k := k
      · simp at hjk
      · simp
      · rfl
    · obtain _ | _ | k := k
      · simp [Fin.ext_iff] at hjk
      · simp [Fin.le_def] at hjk
      · dsimp
        rw [assoc, ← F.map_comp, homOfLE_comp]
  · obtain _ | j := j
    · simp [Fin.ext_iff] at hij
    · obtain _ | k := k
      · simp [Fin.ext_iff] at hjk
      · dsimp
        rw [← F.map_comp, homOfLE_comp]

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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.η.app c.pt ≫ t.lift (newCone D c)) ≫ 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 0 1 ⋯ ⋯ = 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 1 2 ⋯ ⋯ = g

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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 0 2 ⋯ ⋯ = f ≫ g

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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).hom = f ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
⊢ ∀ (j_1 : WalkingMultispan J), colimit.ι I.multispan j_1 ≫ i = colimit.ι I.multispan j_1 ≫ 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 0 0 ⋯ ⋯ = 𝟙 ((mk₂ f g).obj ⟨0, ⋯⟩)

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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 1 1 ⋯ ⋯ = 𝟙 ((mk₂ f g).obj ⟨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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 2 2 ⋯ ⋯ = 𝟙 ((mk₂ f g).obj ⟨2, ⋯⟩)

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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 0 1 ⋯ ⋯ = 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 1 2 ⋯ ⋯ = g

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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 2 3 ⋯ ⋯ = 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 0 3 ⋯ ⋯ = f ≫ g ≫ 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).hom = f ≫ g ≫ 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 0 2 ⋯ ⋯ = f ≫ g

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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 1 3 ⋯ ⋯ = g ≫ h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ sigmaπ I = π I b

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✝
n k l : ℕ
h : k + l ≤ n
x✝ : Fin (l + 1)
i : ℕ
isLt✝ : i < l + 1
⊢ k + i < n + 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✝
n k l : ℕ
h : k + l ≤ n
x✝¹ x✝ : Fin (l + 1)
hij : x✝¹ ⟶ x✝
⊢ (match x✝¹ with
    | ⟨i, isLt⟩ => ⟨k + i, ⋯⟩) ≤
    match x✝ with
    | ⟨i, isLt⟩ => ⟨k + i, ⋯⟩

Tactic:
by

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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.μ.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = (T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c)) ≫ c.π.app j

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {W X Y Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
⊢ ∀ (a : (MultispanShape.prod ι).L),
    I.fst a ≫ c.π ((MultispanShape.prod ι).fst a) = I.snd a ≫ c.π ((MultispanShape.prod ι).snd a)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)

Tactic:
by

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 : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ (T.map (t.lift (T.forget.mapCone s)) ≫ (liftedCone D c t).pt.a) ≫ c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ 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 (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β 0 ⋯ = α ≫ G.map' 0 1 homMk₁._proof_4 ⋯
i : ℕ
hi : i < n + 1
⊢ (F.map' i (i + 1) ⋯ hi ≫
      match ⟨i + 1, ⋯⟩ with
      | ⟨0, isLt⟩ => α
      | ⟨i.succ, hi⟩ => app' β i ⋯) =
    (match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => α
      | ⟨i.succ, hi⟩ => app' β i ⋯) ≫
      G.map' i (i + 1) ⋯ hi

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork I.toLinearOrder
m : c.toLinearOrder.pt ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), c.toLinearOrder.π i ≫ m = s.π i
i : (MultispanShape.prod ι).R
⊢ c.π i ≫ m = c.π i ≫ hc.desc (s.ofLinearOrder h)

Tactic:
by

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 : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J✝), m ≫ (liftedCone D c t).π.app j = s.π.app j
⊢ m = { f := t.lift (T.forget.mapCone s), 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 : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ i < n + 1

Tactic:
by

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
A : adj.toComonad.Coalgebra
⊢ IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))

Tactic:
by

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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ B ⟶ comparisonRightAdjointObj adj A

Tactic:
by

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
⊢ T.η.app c.pt ≫ lambda c t = 𝟙 c.pt

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 : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
⊢ f = g

Tactic:
by

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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ (comparison adj).obj B ⟶ A

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 (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 ⋯
⊢ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.inv 0 ⋯ = α.inv ≫ F.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
by

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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ (fun f ↦ { f := (adj.homEquiv B A.A).symm (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))), h := ⋯ })
      ((fun f ↦ equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯) f) =
    f

Tactic:
by

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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ (fun f ↦ equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯)
      ((fun f ↦ { f := (adj.homEquiv B A.A).symm (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))), h := ⋯ }) f) =
    f

Tactic:
by

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
⊢ T.μ.app c.pt ≫ lambda c t = T.map (lambda c t) ≫ 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 (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 ⋯
⊢ homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯ = 𝟙 F

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X Y Z : WalkingParallelPair} (f : X ⟶ Y) (g : Y ⟶ Z),
    (match Z, X, f ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) =
      (match Y, X, f with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) ≫
        match Z, Y, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WalkingReflexivePair
⊢ Nonempty (StructuredArrow X inclusionWalkingReflexivePair)

Tactic:
by

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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ adj.toComonad.Coalgebra ⥤ C

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 (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 ⋯
⊢ homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w = 𝟙 G

Tactic:
by

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
A : adj.toComonad.Coalgebra
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (G.map A.a) =
    F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A))

Tactic:
by

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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A : adj.toComonad.Coalgebra
⊢ ((comparisonAdjunction adj).counit.app A).f = (beckEqualizer A).lift (counitFork A)

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

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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B)

Tactic:
by

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
j : J
⊢ (T.mapCocone c).ι.app j ≫ T.map (t.desc (T.forget.mapCocone s)) ≫ s.pt.a =
    (T.mapCocone c).ι.app j ≫ (liftedCocone c t).pt.a ≫ t.desc (T.forget.mapCocone 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 : ℕ
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 : Fin (n + 1 + 1)), F.obj i = G.obj i

Tactic:
by

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✝¹ : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ CreatesLimit (parallelPair f g) F

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WalkingReflexivePair
⊢ IsConnected (StructuredArrow X inclusionWalkingReflexivePair)

Tactic:
by

Goal state after: