case mp
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ → HigherFacesVanish q φ

case mpr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
⊢ HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ ↔ HigherFacesVanish q φ
constructor
case mp
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q φ
case mp
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ → HigherFacesVanish q φ
intro hφ
case mp
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))
case mp
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q φ
rw [← hφ]
case mp.v
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (n + 1))
case mp
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))
apply HigherFacesVanish.of_comp
no goals
case mp.v
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (n + 1))
apply HigherFacesVanish.of_P
no goals
case mpr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
⊢ HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
exact HigherFacesVanish.comp_P_eq_self