print(e) for the crashing expression in remove_unnnecessary_casts

expr.lean

category_theory.limits.wide_pullback_shape.hom.rec.{succ v₂ v₁}
    category_theory.limits.walking_pair.{v₁}
    (fun (t_1 : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (t_2 : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (ᾰ : category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} t_1 t_2), ((eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} X t_1) -> (eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z t_2) -> (heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} t_1 t_2) ᾰ) -> (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) Z))))
    (eq.rec.{succ v₂ succ v₁} category_theory.limits.walking_cospan.{v₁} X (fun (ᾰ_1 : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}), ((eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z ᾰ_1) -> (heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1 ᾰ_1) (category_theory.category_struct.id.{v₁ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (category_theory.limits.wide_pullback_shape.struct.{v₁} category_theory.limits.walking_pair.{v₁}) ᾰ_1)) -> (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) Z)))) (fun (H_2 : eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z X), (eq.rec.{(max (succ v₁) (succ v₂)) succ v₁} category_theory.limits.walking_cospan.{v₁} X (fun {Y : category_theory.limits.walking_cospan.{v₁}}, (Pi (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Y) (H_3 : heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Y) ᾰ (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X X) (category_theory.category_struct.id.{v₁ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (category_theory.limits.wide_pullback_shape.struct.{v₁} category_theory.limits.walking_pair.{v₁}) X)), (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) Y)))) (fun (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X X) (H_3 : heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X X) ᾰ (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X X) (category_theory.category_struct.id.{v₁ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (category_theory.limits.wide_pullback_shape.struct.{v₁} category_theory.limits.walking_pair.{v₁}) X)), (category_theory.limits.walking_cospan.hom.id.{v₂} (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X))) Z (eq.symm.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z X H_2) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g))))
    (fun (ᾰ_1 : category_theory.limits.walking_pair.{v₁}) (H_1 : eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} X (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1)), (eq.rec.{(max (succ v₁) (succ v₂)) succ v₁} category_theory.limits.walking_cospan.{v₁} (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) (fun {X : category_theory.limits.walking_cospan.{v₁}}, (Pi (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (H_2 : eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z (option.none.{v₁} category_theory.limits.walking_pair.{v₁})) (H_3 : heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) ᾰ (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) (option.none.{v₁} category_theory.limits.walking_pair.{v₁})) (category_theory.limits.wide_pullback_shape.hom.term.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1)), (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) Z)))) (fun (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) Z) (H_2 : eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z (option.none.{v₁} category_theory.limits.walking_pair.{v₁})), (eq.rec.{(max (succ v₁) (succ v₂)) succ v₁} category_theory.limits.walking_cospan.{v₁} (option.none.{v₁} category_theory.limits.walking_pair.{v₁}) (fun {Y : category_theory.limits.walking_cospan.{v₁}}, (Pi (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) Y) (H_3 : heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) Y) ᾰ (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) (option.none.{v₁} category_theory.limits.walking_pair.{v₁})) (category_theory.limits.wide_pullback_shape.hom.term.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1)), (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂} ᾰ_1) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) Y)))) (fun (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) (option.none.{v₁} category_theory.limits.walking_pair.{v₁})) (H_3 : heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) (option.none.{v₁} category_theory.limits.walking_pair.{v₁})) ᾰ (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) (option.none.{v₁} category_theory.limits.walking_pair.{v₁})) (category_theory.limits.wide_pullback_shape.hom.term.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1)), (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ_1 : category_theory.limits.walking_pair.{v₁}), (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂} ᾰ_1) category_theory.limits.walking_cospan.one.{v₂})) category_theory.limits.walking_cospan.hom.inl.{v₂} category_theory.limits.walking_cospan.hom.inr.{v₂} ᾰ_1)) Z (eq.symm.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z (option.none.{v₁} category_theory.limits.walking_pair.{v₁}) H_2) ᾰ)) X (eq.symm.{succ v₁} category_theory.limits.walking_cospan.{v₁} X (option.some.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1) H_1) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g)))
    X
    Z
    (eq.rec.{succ v₁ succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) X (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ Z)) (eq.rec.{succ v₁ succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) Z (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X ᾰ)) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) Z (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z)) X (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} X))
    (eq.rec.{0 succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) X (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} X ᾰ)) (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} X) X (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} X))
    (eq.rec.{0 succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) Z (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z ᾰ)) (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z) Z (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z))
    (eq.drec.{0 succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) X (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}} (e_3 : eq.{succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) X ᾰ), (heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ Z) (eq.rec.{succ v₁ succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) X (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ Z)) (eq.rec.{succ v₁ succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) Z (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X ᾰ)) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) Z (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z)) ᾰ e_3))) (eq.drec.{0 succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) Z (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}} (e_4 : eq.{succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) Z ᾰ), (heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X ᾰ) (eq.rec.{succ v₁ succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) X (fun {ᾰ_1 : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1 ᾰ)) (eq.rec.{succ v₁ succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) Z (fun {ᾰ : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}}, (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X ᾰ)) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) ᾰ e_4) X (eq.refl.{succ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) X)))) (heq.refl.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g)) Z (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z)) X (eq.refl.{succ v₁} category_theory.limits.walking_cospan.{v₁} X))

-- The eq.rec on line 4 has only four arguments. Here it is with line breaks:
    
eq.rec.{succ v₂ succ v₁}
    category_theory.limits.walking_cospan.{v₁}
    X
    (fun (ᾰ_1 : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}), ((eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z ᾰ_1) -> (heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g) (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} ᾰ_1 ᾰ_1) (category_theory.category_struct.id.{v₁ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (category_theory.limits.wide_pullback_shape.struct.{v₁} category_theory.limits.walking_pair.{v₁}) ᾰ_1)) -> (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) Z))))
    (fun (H_2 : eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z X), (eq.rec.{(max (succ v₁) (succ v₂)) succ v₁} category_theory.limits.walking_cospan.{v₁} X (fun {Y : category_theory.limits.walking_cospan.{v₁}}, (Pi (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Y) (H_3 : heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Y) ᾰ (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X X) (category_theory.category_struct.id.{v₁ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (category_theory.limits.wide_pullback_shape.struct.{v₁} category_theory.limits.walking_pair.{v₁}) X)), (quiver.hom.{succ v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category_struct.to_quiver.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.category.to_category_struct.{v₂ v₂} category_theory.limits.walking_cospan.{v₂} (category_theory.limits.wide_pullback_shape.category.{v₂} category_theory.limits.walking_pair.{v₂}))) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X) (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) Y)))) (fun (ᾰ : quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X X) (H_3 : heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X X) ᾰ (category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} X X) (category_theory.category_struct.id.{v₁ v₁} (category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (category_theory.limits.wide_pullback_shape.struct.{v₁} category_theory.limits.walking_pair.{v₁}) X)), (category_theory.limits.walking_cospan.hom.id.{v₂} (option.rec.{succ v₂ v₁} category_theory.limits.walking_pair.{v₁} (fun (ᾰ : category_theory.limits.walking_cospan.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.one.{v₂} (category_theory.limits.walking_pair.rec.{succ v₂ v₁} (fun (ᾰ : category_theory.limits.walking_pair.{v₁}), category_theory.limits.walking_cospan.{v₂}) category_theory.limits.walking_cospan.left.{v₂} category_theory.limits.walking_cospan.right.{v₂}) X))) Z (eq.symm.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z X H_2) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁})) X Y Z f g)))