Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

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

pp: case init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
Z✝ : WidePushoutShape J
j✝ : J
g : some j✝ ⟶ Z✝
⊢ Hom.casesOn (motive := fun a a_1 x ↦
      none = a → Z✝ = a_1 → Hom.init j✝ ≫ g ≍ x → (Option.casesOn none B objs ⟶ Option.casesOn Z✝ B objs))
      (Hom.init j✝ ≫ g)
      (fun X h ↦
        Eq.ndrec (motive := fun X ↦
          Z✝ = X → Hom.init j✝ ≫ g ≍ Hom.id X → (Option.casesOn none B objs ⟶ Option.casesOn Z✝ 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✝ ≫ g))
          h)
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ 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✝ ≫ g))
      ⋯ ⋯ ⋯ =
    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 → Z✝ = a_1 → g ≍ x → (Option.casesOn (some j✝) B objs ⟶ Option.casesOn Z✝ B objs)) g
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦
            Z✝ = X → g ≍ Hom.id X → (Option.casesOn (some j✝) B objs ⟶ Option.casesOn Z✝ 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)) ⋯ g)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ 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)
            ⋯ g)
        ⋯ ⋯ ⋯

Tactic:
· simp only [hom_id, Category.id_comp]; congr

Goal state after:
case init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
Z✝ : WidePushoutShape J
j✝ : J
g : some j✝ ⟶ Z✝
⊢ Hom.casesOn (motive := fun a a_1 x ↦
      none = a → Z✝ = a_1 → Hom.init j✝ ≫ g ≍ x → (Option.casesOn none B objs ⟶ Option.casesOn Z✝ B objs))
      (Hom.init j✝ ≫ g)
      (fun X h ↦
        Eq.ndrec (motive := fun X ↦
          Z✝ = X → Hom.init j✝ ≫ g ≍ Hom.id X → (Option.casesOn none B objs ⟶ Option.casesOn Z✝ 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✝ ≫ g))
          h)
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ 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✝ ≫ g))
      ⋯ ⋯ ⋯ =
    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 → Z✝ = a_1 → g ≍ x → (Option.casesOn (some j✝) B objs ⟶ Option.casesOn Z✝ B objs)) g
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦
            Z✝ = X → g ≍ Hom.id X → (Option.casesOn (some j✝) B objs ⟶ Option.casesOn Z✝ 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)) ⋯ g)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ 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)
            ⋯ g)
        ⋯ ⋯ ⋯