case h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ f.app Δ = g.app Δ
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
⊢ f = g
ext Δ
case h.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), ιSummand s A ≫ f.app Δ = ιSummand s A ≫ g.app Δ
case h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ f.app Δ = g.app Δ
apply s.hom_ext'
case h.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ f.app Δ = ιSummand s A ≫ g.app Δ
case h.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), ιSummand s A ≫ f.app Δ = ιSummand s A ≫ g.app Δ
intro A
case h.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝ : IndexSet Δ✝
Δ : SimplexCategory
A : IndexSet { unop := Δ }
⊢ ιSummand s A ≫ f.app { unop := Δ } = ιSummand s A ≫ g.app { unop := Δ }
case h.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ f.app Δ = ιSummand s A ≫ g.app Δ
induction' Δ using Opposite.rec with Δ
case h.h.mk.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ f.app { unop := [n] } = ιSummand s A ≫ g.app { unop := [n] }
case h.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝ : IndexSet Δ✝
Δ : SimplexCategory
A : IndexSet { unop := Δ }
⊢ ιSummand s A ≫ f.app { unop := Δ } = ιSummand s A ≫ g.app { unop := Δ }
induction' Δ using SimplexCategory.rec with n
case h.h.mk.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ f.app { unop := [n] } = ιSummand s A ≫ g.app { unop := [n] }
case h.h.mk.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ f.app { unop := [n] } = ιSummand s A ≫ g.app { unop := [n] }
dsimp
no goals
case h.h.mk.h
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ f.app { unop := [n] } = ιSummand s A ≫ g.app { unop := [n] }
simp only [s.ιSummand_comp_app, h]