C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i =>
          if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
          else WidePullback.π (fun x => f.hom) (Fin.pred i x))
        (_ :
          ∀ (i : Fin (SimplexCategory.len [n + 1].op.unop + 1)),
            (fun i =>
                    if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
                    else WidePullback.π (fun x => f.hom) (Fin.pred i x))
                  i ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.π (fun x => f.hom) (Fin.succ i) =
    WidePullback.π (fun x => f.hom) i
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.succ i) = WidePullback.π (fun x => f.hom) i
dsimp [ExtraDegeneracy.s]
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (if x : Fin.succ i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred (Fin.succ i) x)) =
    WidePullback.π (fun x => f.hom) i
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i =>
          if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
          else WidePullback.π (fun x => f.hom) (Fin.pred i x))
        (_ :
          ∀ (i : Fin (SimplexCategory.len [n + 1].op.unop + 1)),
            (fun i =>
                    if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
                    else WidePullback.π (fun x => f.hom) (Fin.pred i x))
                  i ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.π (fun x => f.hom) (Fin.succ i) =
    WidePullback.π (fun x => f.hom) i
simp only [WidePullback.lift_π]
case inl
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
h : Fin.succ i = 0
⊢ (WidePullback.base fun x => f.hom) ≫ S.section_ = WidePullback.π (fun x => f.hom) i

case inr
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
h : ¬Fin.succ i = 0
⊢ WidePullback.π (fun x => f.hom) (Fin.pred (Fin.succ i) h) = WidePullback.π (fun x => f.hom) i
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (if x : Fin.succ i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred (Fin.succ i) x)) =
    WidePullback.π (fun x => f.hom) i
split_ifs with h
no goals
case inl
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
h : Fin.succ i = 0
⊢ (WidePullback.base fun x => f.hom) ≫ S.section_ = WidePullback.π (fun x => f.hom) i
simp only [Fin.ext_iff, Fin.val_succ, Fin.val_zero, add_eq_zero, and_false] at h
no goals
case inr
C : Type u_2
inst✝¹ : Category C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
h : ¬Fin.succ i = 0
⊢ WidePullback.π (fun x => f.hom) (Fin.pred (Fin.succ i) h) = WidePullback.π (fun x => f.hom) i
simp only [Fin.pred_succ]