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

Tactic:
;

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