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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.π.app (WalkingMulticospan.right b) = g ≫ K.π.app (WalkingMulticospan.right b)

Tactic:
dsimp

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.π.app (WalkingMulticospan.right b) = g ≫ K.π.app (WalkingMulticospan.right b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.snd a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.left (J.snd a✝) with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

Tactic:
dsimp

Goal state after:
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ 𝟙 a.pt ≫ a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a✝ = (a.ι ≫ c.proj (J.snd a✝)) ≫ I.snd a✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.id (WalkingMultispan.left a✝))

Tactic:
dsimp

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.multispan.map (𝟙 (WalkingMultispan.left a✝)) ≫ I.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.fst a✝) ≫
      match WalkingMultispan.right (J.fst a✝) with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.fst a✝)

Tactic:
dsimp

Goal state after:
case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.snd a✝) ≫
      match WalkingMultispan.right (J.snd a✝) with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.snd a✝)

Tactic:
dsimp

Goal state after:
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.snd a✝ ≫ π (J.snd a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.R
⊢ (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) =
    (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a) ≫
      ((Functor.const (WalkingMultispan J)).obj P).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))

Tactic:
dsimp

Goal state after:
case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.R
⊢ I.multispan.map (𝟙 (WalkingMultispan.right a✝)) ≫ π a✝ = π a✝ ≫ 𝟙 P
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (1 + 1)
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app i = eqToHom ⋯

Tactic:
by fin_cases i <;> rfl

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
h : L ⊣ R
X : C
⊢ (L ⋙ R).map ((whiskerRight (L.whiskerLeft h.counit) R).app X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X =
    (whiskerRight (L.whiskerLeft h.counit) R).app ((L ⋙ R).obj X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (h.counit.app (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)) =
    R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X))
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
h : L ⊣ R
X : C
⊢ (L ⋙ R).map (h.unit.app X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X = 𝟙 ((L ⋙ R).obj ((𝟭 C).obj X))

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (h.unit.app X)) ≫ R.map (h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
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
h : L ⊣ R
X : D
⊢ (whiskerRight (R.whiskerLeft h.unit) L).app X ≫ (R ⋙ L).map ((whiskerRight (R.whiskerLeft h.unit) L).app X) =
    (whiskerRight (R.whiskerLeft h.unit) L).app X ≫ (whiskerRight (R.whiskerLeft h.unit) L).app ((R ⋙ L).obj X)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (L.map (h.unit.app (R.obj X)))) =
    L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X))))
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
h : L ⊣ R
X : D
⊢ (whiskerRight (R.whiskerLeft h.unit) L).app X ≫ (R ⋙ L).map (h.counit.app X) = 𝟙 ((R ⋙ L).obj X)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
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
h : L ⊣ R
X : D
⊢ h.toMonad.μ.app (R.obj X) ≫ R.map (h.counit.app X) = h.toMonad.map (R.map (h.counit.app X)) ≫ R.map (h.counit.app X)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (h.counit.app (L.obj (R.obj X))) ≫ R.map (h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0, hj⟩ hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

Tactic:
dsimp

Goal state after:
case zero.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f 0 ⟨k, hk⟩ ⋯ = 𝟙 X ≫ map F f 0 ⟨k, hk⟩ hjk
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
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ h.toMonad.map (R.map f) ≫ { A := R.obj Y✝, a := R.map (h.counit.app Y✝), unit := ⋯, assoc := ⋯ }.a =
    { A := R.obj X✝, a := R.map (h.counit.app X✝), unit := ⋯, assoc := ⋯ }.a ≫ R.map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y✝) = R.map (h.counit.app X✝) ≫ R.map f
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
h : L ⊣ R
X : C
⊢ L.map (h.unit.app X) ≫ h.toComonad.δ.app (L.obj X) = L.map (h.unit.app X) ≫ h.toComonad.map (L.map (h.unit.app X))

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (h.unit.app X) ≫ L.map (h.unit.app (R.obj (L.obj X))) =
    L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))
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
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ { A := L.obj X✝, a := L.map (h.unit.app X✝), counit := ⋯, coassoc := ⋯ }.a ≫ h.toComonad.map (L.map f) =
    L.map f ≫ { A := L.obj Y✝, a := L.map (h.unit.app Y✝), counit := ⋯, coassoc := ⋯ }.a

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ L.map (h.unit.app X✝) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y✝)
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✝ : Reflective R
⊢ IsIso (reflectorAdjunction R).toMonad.μ

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ IsIso (whiskerRight ((reflector R).whiskerLeft (reflectorAdjunction R).counit) R)
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
⊢ IsIso (coreflectorAdjunction R).toComonad.δ

Tactic:
dsimp

Goal state after:
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
⊢ IsIso (whiskerRight ((coreflector R).whiskerLeft (coreflectorAdjunction R).unit) R)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
dsimp

Goal state after:
case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k + 1, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨k + 1, hk⟩ hjk

Tactic:
dsimp

Goal state after:
case succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯)
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:
dsimp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ (T.map (t.lift (T.forget.mapCone s)) ≫ t.lift (newCone D c)) ≫ c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j
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
⊢ (adj.homEquiv B (adj.toComonad.obj A.A))
      (((comparison adj).obj B).a ≫
        adj.toComonad.map ((adj.homEquiv B A.A).symm (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))))) =
    (adj.homEquiv B (adj.toComonad.obj A.A))
      ((adj.homEquiv B A.A).symm (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))) ≫ A.a)

Tactic:
simp only [Adjunction.toComonad_coe, Functor.comp_obj, comparison_obj_A, comparison_obj_a,
          Adjunction.homEquiv_counit, Functor.map_comp, Category.assoc,
          Functor.comp_map, Adjunction.homEquiv_unit, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality, Adjunction.right_triangle_components_assoc]

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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ adj.unit.app (G.obj A.A) =
    f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ G.map A.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 (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 ⋯
⊢ F.map' 0 1 homMk₁._proof_4 ⋯ ≫ 𝟙 (F.δ₀.obj ⟨0, ⋯⟩) = F.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
dsimp

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

Tactic:
dsimp

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
A B : J
f : A ⟶ B
⊢ (D.map f).f ≫ c.ι.app B = c.ι.app A ≫ 𝟙 c.pt