Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case left.left.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
a : J.L
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left a)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.left a)

pp: case left.right.fst
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst b')))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left (J.fst b'))) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b')

pp: case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd b')))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left (J.snd b'))) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b')

pp: case right.right.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.right b)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b)

Tactic:
· simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl

Goal state after:
case left.right.fst
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst b')))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left (J.fst b'))) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b')

case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd b')))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left (J.snd b'))) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b')

case right.right.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.right b)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b)