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 : ℕ
⊢ 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) 0 =
    (WidePullback.base fun x => f.hom) ≫ S.section_
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 : ℕ
⊢ s f S n ≫ WidePullback.π (fun x => f.hom) 0 = (WidePullback.base fun x => f.hom) ≫ S.section_
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 : ℕ
⊢ (if h : True then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred 0 (_ : ¬0 = 0))) =
    (WidePullback.base fun x => f.hom) ≫ S.section_
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 : ℕ
⊢ 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) 0 =
    (WidePullback.base fun x => f.hom) ≫ S.section_
simp only [WidePullback.lift_π]
no goals
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 : ℕ
⊢ (if h : True then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred 0 (_ : ¬0 = 0))) =
    (WidePullback.base fun x => f.hom) ≫ S.section_
rfl