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✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
⊢ Multifork (ofParallelHoms J f g) ≌ Fork 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
F G : ComposableArrows C 0
f : F ⟶ G
x✝ : IsIso (f.app 0)
i : Fin (0 + 1)
⊢ IsIso (f.app i)

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
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
c : Fork f g
a : J.L
⊢ ((multiforkOfParallelHomsEquivFork J f g).inverse.obj c).ι a = 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
F G : ComposableArrows C 0
f : F ⟶ G
⊢ IsIso f ↔ IsIso (f.app 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
F G : ComposableArrows C 0
h : F.obj' 0 homMk₀._proof_1 = G.obj 0
i : ℕ
hi : i < 0
⊢ F.map' i (i + 1) ⋯ hi = eqToHom ⋯ ≫ G.map' i (i + 1) ⋯ hi ≫ eqToHom ⋯

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
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = I.fst a ≫ K.π (J.fst 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 1
left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
i : ℕ
hi : i < 1
⊢ i = 0

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
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (J.snd 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 1
left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ ∀ (i : ℕ) (hi : i < 1),
    (F.map' i (i + 1) ⋯ hi ≫
        match ⟨i + 1, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) =
      (match ⟨i, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) ≫
        G.map' i (i + 1) ⋯ hi

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
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4
h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5
⊢ φ = φ'

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 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.inv = left.inv ≫ F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5

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
F G : ComposableArrows C 1
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1)
i : Fin (1 + 1)
⊢ IsIso (f.app i)

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
F G : ComposableArrows C 1
f : F ⟶ G
⊢ IsIso f ↔ IsIso (f.app 0) ∧ IsIso (f.app 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
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ (eqToIso right).hom =
    (eqToIso left).hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5

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
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)
⊢ F.obj i = G.obj i

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

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 1
⊢ X.hom = eqToHom ⋯ ≫ (mk₁ (X.map' 0 1 ⋯ ⋯)).hom ≫ 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₀' X₀ X₁ : C
h : X₀' = X₀
f : X₀ ⟶ X₁
⊢ mk₁ (eqToHom h ≫ f) = mk₁ 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
X₀ X₁ X₁' : C
f : X₀ ⟶ X₁
h : X₁ = X₁'
⊢ mk₁ (f ≫ eqToHom h) = mk₁ 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
X : ComposableArrows C 1
⊢ (mk₁ X.hom).hom = eqToHom ⋯ ≫ X.hom ≫ 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 : ComposableArrows C 1
⊢ ((fun f ↦ mk₁ f.hom) ((fun F ↦ Arrow.mk F.hom) F)).hom = eqToHom ⋯ ≫ F.hom ≫ 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
X : C
f : X ⟶ F.left
i : ℕ
hi : i + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩
⊢ i ≤ 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 : C
f : X ⟶ F.left
⊢ 0 ≤ 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 : C
f : X ⟶ F.left
⊢ 1 ≤ 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 : C
f : X ⟶ F.left
⊢ 0 ≤ 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 : C
f : X ⟶ F.left
⊢ 0 + 1 < n + 1 + 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 : C
f : X ⟶ F.left
⊢ 0 ≤ ⟨0 + 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 : C
f : X ⟶ F.left
j : ℕ
hj : j + 2 < n + 1 + 1
⊢ 0 ≤ ⟨j + 2, hj⟩

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 : C
f : X ⟶ F.left
j : ℕ
hj : j + 1 < n + 1 + 1
⊢ 1 ≤ ⟨j + 1, hj⟩

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 : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ i ≤ i

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
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:
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
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:
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
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)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) =
      (match X with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) ≫
        ((Functor.const (WalkingMultispan J)).obj P).map f

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
K : Multicofork I
a : J.L
⊢ I.fst a ≫ K.π (J.fst a) = I.snd a ≫ K.π (J.snd 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 : ComposableArrows C n
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)

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
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
    rw [← L.map_comp]
    simp

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 : 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:
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
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
    rw [← L.map_comp]
    simp

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

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
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
⊢ ∀ (s : Cocone I.multispan) (j : WalkingMultispan J), K.ι.app j ≫ desc s = s.ι.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
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ adj.unit ≫ i.hom ≫ (adj.toMonad.transport i).μ = 𝟙 (𝟭 C)

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
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ (i.hom ≫ (adj.toMonad.transport i).μ) ≫ adj.unit = 𝟙 (L ⋙ R)

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
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
⊢ ∀ (s : Cocone I.multispan) (m : K.pt ⟶ s.pt), (∀ (j : WalkingMultispan J), K.ι.app j ≫ m = s.ι.app j) → m = desc s

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
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ adj.counit ≫ (adj.toComonad.transport j).δ ≫ j.inv = 𝟙 (R ⋙ L)

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
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
⊢ f = g

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
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ ((adj.toComonad.transport j).δ ≫ j.inv) ≫ adj.counit = 𝟙 (𝟭 D)

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
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π

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
K✝ : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K : Multicofork I
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd 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
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:
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
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:
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
T : Monad C
x✝¹ x✝ : T.Algebra
f : (Monad.comparison T.adj).obj x✝¹ ⟶ (Monad.comparison T.adj).obj x✝
⊢ T.map f.f ≫ x✝.a = x✝¹.a ≫ f.f

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
T : Monad C
X : T.adj.toMonad.Algebra
⊢ T.η.app X.A ≫ X.a = 𝟙 X.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
L : C ⥤ D
R : D ⥤ C
T : Monad C
X : T.adj.toMonad.Algebra
⊢ T.μ.app X.A ≫ X.a = T.map X.a ≫ X.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
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:
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
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:
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
G : Comonad C
X✝ Y✝ : G.Coalgebra
f : (Comonad.comparison G.adj).obj X✝ ⟶ (Comonad.comparison G.adj).obj Y✝
⊢ X✝.a ≫ G.map f.f = f.f ≫ Y✝.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
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X : G.adj.toComonad.Coalgebra
⊢ X.a ≫ G.ε.app X.A = 𝟙 X.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
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X : G.adj.toComonad.Coalgebra
⊢ X.a ≫ G.δ.app X.A = X.a ≫ G.map X.a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (adj.unit.app (G.obj B)) ≫ F.map (G.map (adj.counit.app B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))

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✝ : Reflective R
⊢ IsIso (reflectorAdjunction R).toMonad.μ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
⊢ HasCoequalizer f g

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
⊢ IsIso (coreflectorAdjunction R).toComonad.δ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
⊢ HasEqualizer f g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasCoequalizers C
A B : C
f g : A ⟶ B
x✝ : IsReflexivePair f g
⊢ HasCoequalizer f g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasEqualizers C
A B : C
f g : A ⟶ B
x✝ : IsCoreflexivePair f g
⊢ HasEqualizer f g

Tactic:
by

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

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

Tactic:
by

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

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

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✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ X.a ≫ (reflectorAdjunction R).unit.app X.A = 𝟙 ((reflector 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
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
        | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
      (match X with
        | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
        | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
        ((Functor.const (WalkingMultispan J)).obj a.pt).map f

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✝ : Reflective R
⊢ (Monad.comparison (reflectorAdjunction R)).EssSurj

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 : L ⊣ R
X✝ Y✝ : D
f : (Monad.comparison adj).obj X✝ ⟶ (Monad.comparison adj).obj Y✝
⊢ (Monad.comparison adj).map (R.preimage f.f) = f

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
K✝ : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K K' : Multicofork I
e : K.pt ≅ K'.pt
h : ∀ (i : J.R), K.π i ≫ e.hom = K'.π i
⊢ ∀ (j : WalkingMultispan J), K.ι.app j ≫ e.hom = K'.ι.app j

Tactic:
by

Goal state after: