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

Goal state before:
pp: case left
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
K : Multifork I
a✝ : J.L
⊢ ((𝟭 (Multifork I)).obj K).π.app (WalkingMulticospan.left a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.left a✝)

pp: case right
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
K : Multifork I
a✝ : J.R
⊢ ((𝟭 (Multifork I)).obj K).π.app (WalkingMulticospan.right a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.right a✝)

Tactic:
<;>

Goal state after:
case left
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
K : Multifork I
a✝ : J.L
⊢ ((𝟭 (Multifork I)).obj K).π.app (WalkingMulticospan.left a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.left a✝)

case right
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
K : Multifork I
a✝ : J.R
⊢ ((𝟭 (Multifork I)).obj K).π.app (WalkingMulticospan.right a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.right a✝)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case «0»
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)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case «1»
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)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
<;>

Goal state after:
case «0»
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)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
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)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case «0»
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.obj ((fun i ↦ i) ⟨0, ⋯⟩) = G.obj ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
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.obj ((fun i ↦ i) ⟨1, ⋯⟩) = G.obj ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
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.obj ((fun i ↦ i) ⟨0, ⋯⟩) = G.obj ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
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.obj ((fun i ↦ i) ⟨1, ⋯⟩) = G.obj ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case «0»
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 ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨0, ⋯⟩) = eqToHom ⋯

pp: case «1»
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 ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨1, ⋯⟩) = eqToHom ⋯

Tactic:
<;>

Goal state after:
case «0»
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 ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨0, ⋯⟩) = eqToHom ⋯

case «1»
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 ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨1, ⋯⟩) = eqToHom ⋯
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.left a✝)) ≫ I.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

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.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

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.snd a✝ ≫ π (J.snd a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

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.right a✝)) ≫ π a✝ = π a✝ ≫ 𝟙 P

Tactic:
<;>

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

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

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

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: case zero
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
⊢ map F f ⟨0, hi⟩ ⟨0, hi⟩ ⋯ = 𝟙 (obj F X ⟨0, hi⟩)

pp: case 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
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨n✝ + 1, hi⟩ ⋯ = 𝟙 (obj F X ⟨n✝ + 1, hi⟩)

Tactic:
<;>

Goal state after:
case zero
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
⊢ map F f ⟨0, hi⟩ ⟨0, hi⟩ ⋯ = 𝟙 (obj F X ⟨0, hi⟩)

case 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
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨n✝ + 1, hi⟩ ⋯ = 𝟙 (obj F X ⟨n✝ + 1, hi⟩)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
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
a✝ : J.L
⊢ K.ι.app (WalkingMultispan.left a✝) ≫ f = K.ι.app (WalkingMultispan.left a✝) ≫ g

pp: case right
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
a✝ : J.R
⊢ K.ι.app (WalkingMultispan.right a✝) ≫ f = K.ι.app (WalkingMultispan.right a✝) ≫ g

Tactic:
<;>

Goal state after:
case left
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
a✝ : J.L
⊢ K.ι.app (WalkingMultispan.left a✝) ≫ f = K.ι.app (WalkingMultispan.left a✝) ≫ g

case right
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
a✝ : J.R
⊢ K.ι.app (WalkingMultispan.right a✝) ≫ f = K.ι.app (WalkingMultispan.right a✝) ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left
⊢ (Hom.id one).comp Hom.left = Hom.left

pp: case right
⊢ (Hom.id one).comp Hom.right = Hom.right

pp: case reflexion
⊢ (Hom.id zero).comp Hom.reflexion = Hom.reflexion

pp: case leftCompReflexion
⊢ (Hom.id one).comp Hom.leftCompReflexion = Hom.leftCompReflexion

pp: case rightCompReflexion
⊢ (Hom.id one).comp Hom.rightCompReflexion = Hom.rightCompReflexion

pp: case id
X✝ : WalkingReflexivePair
⊢ (Hom.id X✝).comp (Hom.id X✝) = Hom.id X✝

Tactic:
<;>

Goal state after:
case left
⊢ (Hom.id one).comp Hom.left = Hom.left

case right
⊢ (Hom.id one).comp Hom.right = Hom.right

case reflexion
⊢ (Hom.id zero).comp Hom.reflexion = Hom.reflexion

case leftCompReflexion
⊢ (Hom.id one).comp Hom.leftCompReflexion = Hom.leftCompReflexion

case rightCompReflexion
⊢ (Hom.id one).comp Hom.rightCompReflexion = Hom.rightCompReflexion

case id
X✝ : WalkingReflexivePair
⊢ (Hom.id X✝).comp (Hom.id X✝) = Hom.id X✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left
⊢ Hom.left.comp (Hom.id zero) = Hom.left

pp: case right
⊢ Hom.right.comp (Hom.id zero) = Hom.right

pp: case reflexion
⊢ Hom.reflexion.comp (Hom.id one) = Hom.reflexion

pp: case leftCompReflexion
⊢ Hom.leftCompReflexion.comp (Hom.id one) = Hom.leftCompReflexion

pp: case rightCompReflexion
⊢ Hom.rightCompReflexion.comp (Hom.id one) = Hom.rightCompReflexion

pp: case id
X✝ : WalkingReflexivePair
⊢ (Hom.id X✝).comp (Hom.id X✝) = Hom.id X✝

Tactic:
<;>

Goal state after:
case left
⊢ Hom.left.comp (Hom.id zero) = Hom.left

case right
⊢ Hom.right.comp (Hom.id zero) = Hom.right

case reflexion
⊢ Hom.reflexion.comp (Hom.id one) = Hom.reflexion

case leftCompReflexion
⊢ Hom.leftCompReflexion.comp (Hom.id one) = Hom.leftCompReflexion

case rightCompReflexion
⊢ Hom.rightCompReflexion.comp (Hom.id one) = Hom.rightCompReflexion

case id
X✝ : WalkingReflexivePair
⊢ (Hom.id X✝).comp (Hom.id X✝) = Hom.id X✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : zero.Hom Y✝
⊢ (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)

pp: case right
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : zero.Hom Y✝
⊢ (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)

pp: case reflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)

pp: case leftCompReflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)

pp: case rightCompReflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)

pp: case id
W✝ Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : W✝.Hom Y✝
⊢ ((Hom.id W✝).comp g).comp h = (Hom.id W✝).comp (g.comp h)

Tactic:
<;>

Goal state after:
case left
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : zero.Hom Y✝
⊢ (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)

case right
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : zero.Hom Y✝
⊢ (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)

case reflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)

case leftCompReflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)

case rightCompReflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)

case id
W✝ Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : W✝.Hom Y✝
⊢ ((Hom.id W✝).comp g).comp h = (Hom.id W✝).comp (g.comp h)
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
        rintro (_ | _) (_ | _) (_ | _ | _)
        · simp
        · simp
        · simp [a.condition]
        · simp

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

Goal state before:
pp: case left
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
i : J.L
⊢ K.ι.app (WalkingMultispan.left i) ≫ e.hom = K'.ι.app (WalkingMultispan.left i)

pp: case right
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 : J.R
⊢ K.ι.app (WalkingMultispan.right j) ≫ e.hom = K'.ι.app (WalkingMultispan.right j)

Tactic:
<;>

Goal state after:
case left
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
i : J.L
⊢ K.ι.app (WalkingMultispan.left i) ≫ e.hom = K'.ι.app (WalkingMultispan.left i)

case right
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 : J.R
⊢ K.ι.app (WalkingMultispan.right j) ≫ e.hom = K'.ι.app (WalkingMultispan.right j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
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₂
a✝ : J.L
⊢ (Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.left a✝) ≫ f.hom =
    (Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.left a✝)

pp: case right
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₂
a✝ : J.R
⊢ (Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.right a✝) ≫ f.hom =
    (Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.right a✝)

Tactic:
<;>

Goal state after:
case left
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₂
a✝ : J.L
⊢ (Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.left a✝) ≫ f.hom =
    (Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.left a✝)

case right
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₂
a✝ : J.R
⊢ (Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.right a✝) ≫ f.hom =
    (Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
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
a✝ : J.L
⊢ ((𝟭 (Multicofork I)).obj K).ι.app (WalkingMultispan.left a✝) ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.left a✝)

pp: case right
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
a✝ : J.R
⊢ ((𝟭 (Multicofork I)).obj K).ι.app (WalkingMultispan.right a✝) ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.right a✝)

Tactic:
<;>

Goal state after:
case left
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
a✝ : J.L
⊢ ((𝟭 (Multicofork I)).obj K).ι.app (WalkingMultispan.left a✝) ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.left a✝)

case right
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
a✝ : J.R
⊢ ((𝟭 (Multicofork I)).obj K).ι.app (WalkingMultispan.right a✝) ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

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

Tactic:
F.map_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ 𝟙 (F.obj zero) = 𝟙 (F.obj zero)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
hi : 0 < n + 1 + 1
⊢ f.app ⟨0, hi⟩ = g.app ⟨0, hi⟩

pp: case succ
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
⊢ f.app ⟨i + 1, hi⟩ = g.app ⟨i + 1, hi⟩

Tactic:
· exact h₀

Goal state after:
case succ
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
⊢ f.app ⟨i + 1, hi⟩ = g.app ⟨i + 1, hi⟩
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

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

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

Tactic:
· exact h₀

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom ≫ app₁.inv =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_246✝

Tactic:
app₁.hom_inv_id,

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 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ 𝟙 (f.obj' 1 _proof_246✝) =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_246✝