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

Goal state before:
pp: case inl
J : MultispanShape
val✝ : J.L
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inl val✝)) =
    Sum.inl val✝

pp: case inr
J : MultispanShape
val✝ : J.R
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inr val✝)) =
    Sum.inr val✝

Tactic:
<;>

Goal state after:
case inl
J : MultispanShape
val✝ : J.L
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inl val✝)) =
    Sum.inl val✝

case inr
J : MultispanShape
val✝ : J.R
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inr val✝)) =
    Sum.inr val✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inl
J : MultispanShape
val✝ : WalkingMultispan J
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inl val✝)) =
    Sum.inl val✝

pp: case inr.inl
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inl val✝))) =
    Sum.inr (Sum.inl val✝)

pp: case inr.inr
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inr val✝))) =
    Sum.inr (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
J : MultispanShape
val✝ : WalkingMultispan J
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inl val✝)) =
    Sum.inl val✝

case inr.inl
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inl val✝))) =
    Sum.inr (Sum.inl val✝)

case inr.inr
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inr val✝))) =
    Sum.inr (Sum.inr val✝)
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
a✝ : J.L
⊢ (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝, 𝟙 (WalkingMulticospan.left a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)

pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.R
⊢ (match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝, 𝟙 (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.L
⊢ (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝, 𝟙 (WalkingMulticospan.left a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.R
⊢ (match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝, 𝟙 (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)
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
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, 𝟙 (WalkingMultispan.left a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)

pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.R
⊢ (match WalkingMultispan.right a✝, WalkingMultispan.right a✝, 𝟙 (WalkingMultispan.right a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, 𝟙 (WalkingMultispan.left a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.R
⊢ (match WalkingMultispan.right a✝, WalkingMultispan.right a✝, 𝟙 (WalkingMultispan.right a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: case left.left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ (((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map { down := { down := ⋯ } } ≫
      Discrete.casesOn { as := WalkingPair.left } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) =
    (Discrete.casesOn { as := WalkingPair.left } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) ≫
      (pair M N).map { down := { down := ⋯ } }

pp: case right.right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ (((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map { down := { down := ⋯ } } ≫
      Discrete.casesOn { as := WalkingPair.right } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) =
    (Discrete.casesOn { as := WalkingPair.right } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) ≫
      (pair M N).map { down := { down := ⋯ } }

Tactic:
<;>

Goal state after:
case left.left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ (((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map { down := { down := ⋯ } } ≫
      Discrete.casesOn { as := WalkingPair.left } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) =
    (Discrete.casesOn { as := WalkingPair.left } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) ≫
      (pair M N).map { down := { down := ⋯ } }

case right.right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ (((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map { down := { down := ⋯ } } ≫
      Discrete.casesOn { as := WalkingPair.right } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) =
    (Discrete.casesOn { as := WalkingPair.right } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) ≫
      (pair M N).map { down := { down := ⋯ } }
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: case left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
      { pt := of R (↑M × ↑N),
              π :=
                {
                  app := fun j ↦
                    Discrete.casesOn j fun j ↦
                      WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                  naturality := ⋯ } }.π.app
        { as := WalkingPair.left } =
    s.π.app { as := WalkingPair.left }

pp: case right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
      { pt := of R (↑M × ↑N),
              π :=
                {
                  app := fun j ↦
                    Discrete.casesOn j fun j ↦
                      WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                  naturality := ⋯ } }.π.app
        { as := WalkingPair.right } =
    s.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
      { pt := of R (↑M × ↑N),
              π :=
                {
                  app := fun j ↦
                    Discrete.casesOn j fun j ↦
                      WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                  naturality := ⋯ } }.π.app
        { as := WalkingPair.left } =
    s.π.app { as := WalkingPair.left }

case right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
      { pt := of R (↑M × ↑N),
              π :=
                {
                  app := fun j ↦
                    Discrete.casesOn j fun j ↦
                      WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                  naturality := ⋯ } }.π.app
        { as := WalkingPair.right } =
    s.π.app { as := WalkingPair.right }
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.pt
w :
  ∀ (j : Discrete J),
    m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.π.app j = s.π.app j
⊢ m = lift f s

Tactic:
ext x j
        exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)

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

Goal state before:
pp: case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝

pp: case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst a✝)

pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝

Tactic:
<;>

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝

case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst a✝)

case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝

pp: case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝

pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.snd a✝

pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝

Tactic:
<;>

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝

case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝

case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.snd a✝

case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝
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
K t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
i : J.L
⊢ t.π.app (WalkingMulticospan.left i) = e.hom ≫ s.π.app (WalkingMulticospan.left i)

pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
j : J.R
⊢ t.π.app (WalkingMulticospan.right j) = e.hom ≫ s.π.app (WalkingMulticospan.right j)

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
i : J.L
⊢ t.π.app (WalkingMulticospan.left i) = e.hom ≫ s.π.app (WalkingMulticospan.left i)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
j : J.R
⊢ t.π.app (WalkingMulticospan.right j) = e.hom ≫ s.π.app (WalkingMulticospan.right j)
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₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a✝ : J.L
⊢ f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.left a✝) =
    (Multifork.ofPiFork 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₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a✝ : J.R
⊢ f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.right a✝) =
    (Multifork.ofPiFork 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₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a✝ : J.L
⊢ f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.left a✝) =
    (Multifork.ofPiFork 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₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a✝ : J.R
⊢ f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.right a✝) =
    (Multifork.ofPiFork K₁).π.app (WalkingMulticospan.right a✝)