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)
        ⋯ ⋯ ⋯

Tactic:
simp only [hom_id, Category.id_comp]

Goal state after:
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.rec (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → 𝟙 X✝ ≫ g ≍ x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
      (fun X h ↦
        Eq.rec (motive := fun x x_1 ↦
          Z✝ = x → 𝟙 X✝ ≫ g ≍ 𝟙 x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun h ↦
            Eq.rec (motive := fun x x_1 ↦
              (f : X✝ ⟶ x) → f ≍ 𝟙 X✝ → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ objs val) X✝)) ⋯ (𝟙 X✝ ≫ g))
          h)
      (fun j h ↦
        Eq.rec (motive := fun x x_1 ↦
          (f : x ⟶ Z✝) →
            Z✝ = some j → f ≍ Hom.init j → (Option.rec B (fun val ↦ objs val) x ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun f h ↦
            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) ⋯ f)
          ⋯ (𝟙 X✝ ≫ g))
      (𝟙 X✝ ≫ g) ⋯ ⋯ ⋯ =
    Hom.rec (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → g ≍ x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
      (fun X h ↦
        Eq.rec (motive := fun x x_1 ↦
          Z✝ = x → g ≍ 𝟙 x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun h ↦
            Eq.rec (motive := fun x x_1 ↦
              (f : X✝ ⟶ x) → f ≍ 𝟙 X✝ → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ objs val) X✝)) ⋯ g)
          h)
      (fun j h ↦
        Eq.rec (motive := fun x x_1 ↦
          (f : x ⟶ Z✝) →
            Z✝ = some j → f ≍ Hom.init j → (Option.rec B (fun val ↦ objs val) x ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun f h ↦
            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) ⋯ f)
          ⋯ g)
      g ⋯ ⋯ ⋯