ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<GOAL>(lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : ‖limNthHom f_compat r - ↑(nthHom f r (max n k))‖ ≤ ↑p ^ (-↑n)<GOAL>(lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}<GOAL>(lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}<GOAL>limNthHom f_compat r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}<GOAL>↑(nthHom f r (max n k)) - ↑((f n) r).val + (limNthHom f_compat r - ↑(nthHom f r (max n k))) ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}<GOAL>↑(nthHom f r (max n k)) - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}<GOAL>↑p ^ n ∣ ↑(nthHom f r (max n k)) - ↑((f n) r).val
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}<GOAL>↑p ^ n = (Int.castRingHom ℤ_[p]) (↑p ^ n)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n k : ℕ<VAR>hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)<VAR>this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}<GOAL>↑(nthHom f r (max n k)) - ↑((f n) r).val = (Int.castRingHom ℤ_[p]) (nthHom f r (max n k) - nthHom f r n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>h : ∀ (i : (Quotient.out o).α), o.familyOfBFamily f i ≤ a<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>f i hi ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>h : ∀ (i : (Quotient.out o).α), o.familyOfBFamily f i ≤ a<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>o.familyOfBFamily f (enum (fun x x_1 => x < x_1) i ⋯) ≤ a
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A : Matrix n n 𝕜<GOAL>A.PosSemidef ↔ ∃ B, A = Bᴴ * B
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>inst✝ : Infinite R<GOAL>#↑Set.univ = #R
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))<GOAL>C.pt.str = ⨅ j, induced (⇑(C.π.app j)) (F.obj j).str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))<GOAL>induced (⇑homeo) (limitConeInfi F).pt.topologicalSpace_coe = ⨅ j, induced (⇑(C.π.app j)) (F.obj j).str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))<GOAL>induced (⇑homeo) (⨅ j, induced ((Types.limitCone (F ⋙ forget TopCat)).π.app j) (F.obj j).str) = ⨅ j, induced (⇑(C.π.app j)) (F.obj j).str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))<GOAL>⨅ i, induced ((Types.limitCone (F ⋙ forget TopCat)).π.app i ∘ ⇑homeo) (F.obj i).str = ⨅ j, induced (⇑(C.π.app j)) (F.obj j).str
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝² : StrongRankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : range v ≤ ↑(span R w)<GOAL>Fintype.card ι ≤ Fintype.card ↑w
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝² : StrongRankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : range v ≤ ↑(span R w)<GOAL>(ι →₀ R) →ₗ[R] ↑w →₀ R
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝² : StrongRankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : range v ≤ ↑(span R w)<GOAL>Injective ⇑?f
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>v : n → α<GOAL>‖row ι v‖₊ = ‖v‖₊
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>φ : (single₀ V).obj X ⟶ C<GOAL>φ.f 0 ≫ C.d 0 1 = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : { f // f ≫ C.d 0 1 = 0 }<VAR>i : ℕ<VAR>hi : (ComplexShape.up ℕ).Rel 0 i<GOAL>↑f ≫ C.d 0 i = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : { f // f ≫ C.d 0 1 = 0 }<VAR>hi : (ComplexShape.up ℕ).Rel 0 1<GOAL>↑f ≫ C.d 0 1 = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<GOAL>Subsingleton P
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<VAR>p : P<VAR>hp : p ∈ s<GOAL>Subsingleton P
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<VAR>p : P<VAR>hp : p ∈ s<VAR>this : s = {p}<GOAL>Subsingleton P
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>p : P<VAR>h₂ : univ.Subsingleton<VAR>hp : p ∈ s<VAR>this : s = {p}<GOAL>Subsingleton P
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>ht : autoParam t.Finite _auto✝<GOAL>s.ncard ≤ (s \ t).ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>ht : autoParam t.Finite _auto✝<VAR>hs : s.Finite<GOAL>s.ncard ≤ (s \ t).ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>ht : autoParam t.Finite _auto✝<VAR>hs : s.Infinite<GOAL>s.ncard ≤ (s \ t).ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>ht : autoParam t.Finite _auto✝<VAR>hs : s.Infinite<GOAL>s.ncard = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommSemiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>x : σ → A<VAR>p : MvPolynomial σ R<VAR>h : Function.Injective ⇑(algebraMap A B)<GOAL>(aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 ≤ x<VAR>hx1 : x ≤ 1<VAR>hz : 0 ≤ z<VAR>hyz : z ≤ y<GOAL>x ^ y ≤ x ^ z
<VAR>y z : ℝ<VAR>n : ℕ<VAR>hz : 0 ≤ z<VAR>hyz : z ≤ y<VAR>hx0 : 0 ≤ 0<VAR>hx1 : 0 ≤ 1<GOAL>0 ^ y ≤ 0 ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 ≤ x<VAR>hx1 : x ≤ 1<VAR>hz : 0 ≤ z<VAR>hyz : z ≤ y<VAR>hx0' : 0 < x<GOAL>x ^ y ≤ x ^ z
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>γ₁ : Sort u_3<VAR>α₂ : Sort u_4<VAR>β₂ : Sort u_5<VAR>γ₂ : Sort u_6<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<VAR>ec : γ₁ ≃ γ₂<VAR>f : α₁ → β₁<VAR>g : β₁ → γ₁<VAR>x✝ : α₂<GOAL>(ea.arrowCongr ec) (g ∘ f) x✝ = ((eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f) x✝
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f✝ f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>x y : M<GOAL>Pi.prod (⇑f) (⇑g) (x + y) = Pi.prod (⇑f) (⇑g) x + Pi.prod (⇑f) (⇑g) y
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f✝ f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>c : R<VAR>x : M<GOAL>{ toFun := Pi.prod ⇑f ⇑g, map_add' := ⋯ }.toFun (c • x) = (RingHom.id R) c • { toFun := Pi.prod ⇑f ⇑g, map_add' := ⋯ }.toFun x
<VAR>α : Type u_1<VAR>inst✝ : OrderedSemiring α<VAR>x : ↑(Icc 0 1)<GOAL>x = 1 ↔ ↑x = 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(homologyFunctor C (up ℤ) 0).homologySequenceδ (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f)) ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁)) n₀ n₁ h = (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).inv.app S.X₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫ (homologyFunctor C (up ℤ) 0).homologySequenceδ (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f)) ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁)) n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ = HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>yoneda.map ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫ (homologyFunctor C (up ℤ) 0).homologySequenceδ (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f)) ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁)) n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁) = yoneda.map (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<GOAL>(yoneda.map ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫ (homologyFunctor C (up ℤ) 0).homologySequenceδ (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f)) ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁)) n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app (Opposite.op A) x = (yoneda.map (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app (Opposite.op A) x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀<GOAL>(yoneda.map ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫ (homologyFunctor C (up ℤ) 0).homologySequenceδ (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f)) ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁)) n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app (Opposite.op A) x = (yoneda.map (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app (Opposite.op A) x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀<GOAL>x ≫ (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫ (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ ≫ (homologyFunctorFactors C (up ℤ) n₁).inv.app S.X₁ ≫ (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ = x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 (S.X₁.homology n₁)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀<GOAL>x ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁) = x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀<GOAL>x ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ = x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀<GOAL>(mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀ ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ = HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀<VAR>a : A' ⟶ S.X₁.X n₁<VAR>b : A' ⟶ S.X₂.X n₀<VAR>hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀<GOAL>(mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀ ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ = HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝¹ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀<VAR>a : A' ⟶ S.X₁.X n₁<VAR>b : A' ⟶ S.X₂.X n₀<VAR>w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0<VAR>hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀<GOAL>(mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀ ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ = HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝¹ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀<VAR>a : A' ⟶ S.X₁.X n₁<VAR>b : A' ⟶ S.X₂.X n₀<VAR>w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0<VAR>hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀<GOAL>(mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀ ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ = HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝¹ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀<VAR>a : A' ⟶ S.X₁.X n₁<VAR>b : A' ⟶ S.X₂.X n₀<VAR>w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0<VAR>hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀<GOAL>(mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀ ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ = S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁