Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case init.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j✝ : J
⊢ Hom.casesOn (motive := fun a a_1 x ↦
      none = a →
        some j✝ = a_1 →
          Hom.init j✝ ≫ Hom.id (some j✝) ≍ x → (Option.casesOn none B objs ⟶ Option.casesOn (some j✝) B objs))
      (Hom.init j✝ ≫ Hom.id (some j✝))
      (fun X h ↦
        Eq.ndrec (motive := fun X ↦
          some j✝ = X →
            Hom.init j✝ ≫ Hom.id (some j✝) ≍ Hom.id X → (Option.casesOn none B objs ⟶ Option.casesOn (some j✝) B objs))
          (fun h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : none ⟶ Y) → f ≍ Hom.id none → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ 𝟙 (Option.casesOn none B objs)) ⋯ (Hom.init j✝ ≫ Hom.id (some j✝)))
          h)
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ some j✝) →
            some j✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn (some j✝) B objs))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ arrows j) ⋯ f)
          ⋯ (Hom.init j✝ ≫ Hom.id (some j✝)))
      ⋯ ⋯ ⋯ =
    Hom.casesOn (motive := fun a a_1 x ↦
        none = a → some j✝ = a_1 → Hom.init j✝ ≍ x → (Option.casesOn none B objs ⟶ Option.casesOn (some j✝) B objs))
        (Hom.init j✝)
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦
            some j✝ = X → Hom.init j✝ ≍ Hom.id X → (Option.casesOn none B objs ⟶ Option.casesOn (some j✝) B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.id none → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn none B objs)) ⋯ (Hom.init j✝))
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ some j✝) →
              some j✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn (some j✝) B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ (Hom.init j✝))
        ⋯ ⋯ ⋯ ≫
      Hom.casesOn (motive := fun a a_1 x ↦
        some j✝ = a →
          some j✝ = a_1 → Hom.id (some j✝) ≍ x → (Option.casesOn (some j✝) B objs ⟶ Option.casesOn (some j✝) B objs))
        (Hom.id (some j✝))
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦
            some j✝ = X →
              Hom.id (some j✝) ≍ Hom.id X → (Option.casesOn (some j✝) B objs ⟶ Option.casesOn (some j✝) B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : some j✝ ⟶ Y) → f ≍ Hom.id (some j✝) → (Option.casesOn (some j✝) B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn (some j✝) B objs)) ⋯ (Hom.id (some j✝)))
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ some j✝) →
              some j✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn (some j✝) B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ (Hom.id (some j✝)))
        ⋯ ⋯ ⋯

Tactic:
simp only [hom_id, Category.comp_id]

Goal state after:
case init.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j✝ : J
⊢ Hom.rec (motive := fun a a_1 x ↦ none = a → some j✝ = a_1 → Hom.init j✝ ≫ 𝟙 (some j✝) ≍ x → (B ⟶ objs j✝))
      (fun X h ↦
        Eq.rec (motive := fun x x_1 ↦ some j✝ = x → Hom.init j✝ ≫ 𝟙 (some j✝) ≍ 𝟙 x → (B ⟶ objs j✝))
          (fun h ↦
            Eq.rec (motive := fun x x_1 ↦ (f : none ⟶ x) → f ≍ 𝟙 none → (B ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ 𝟙 B) ⋯ (Hom.init j✝ ≫ 𝟙 (some j✝)))
          h)
      (fun j h h_1 ↦
        Eq.rec (motive := fun x x_1 ↦ (f : none ⟶ x) → f ≍ Hom.init j → (B ⟶ Option.rec B (fun val ↦ objs val) x))
          (fun f h ↦ arrows j) ⋯ (Hom.init j✝ ≫ 𝟙 (some j✝)))
      (Hom.init j✝ ≫ 𝟙 (some j✝)) ⋯ ⋯ ⋯ =
    arrows j✝