ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Rack R<VAR>a b : Rack.PreEnvelGroup R<GOAL>Rack.PreEnvelGroupRel' R a b → Rack.PreEnvelGroupRel R a b
<VAR>R : Type u<VAR>Rack R<VAR>a : Rack.PreEnvelGroup R<GOAL>Rack.PreEnvelGroupRel R a a
<VAR>R : Type u<VAR>Rack R<VAR>a b : Rack.PreEnvelGroup R<GOAL>Rack.PreEnvelGroupRel R a b → Rack.PreEnvelGroupRel R b a
<VAR>R : Type u<VAR>Rack R<VAR>a b c : Rack.PreEnvelGroup R<GOAL>Rack.PreEnvelGroupRel R a b → Rack.PreEnvelGroupRel R b c → Rack.PreEnvelGroupRel R a c
<VAR>R : Type u_1<VAR>Rack R<VAR>G : Type u_2<VAR>Group G<VAR>f : R →◃ Quandle.Conj G<VAR>a b : Rack.PreEnvelGroup R<GOAL>Rack.PreEnvelGroupRel' R a b → Rack.toEnvelGroup.mapAux f a = Rack.toEnvelGroup.mapAux f b
<VAR>R : Type u_1<VAR>Rack R<VAR>G : Type u_2<VAR>Group G<VAR>f : R →◃ Quandle.Conj G<GOAL>(Quandle.Conj.map (Rack.toEnvelGroup.map f)).comp (Rack.toEnvelGroup R) = f
<VAR>R : Type u_1<VAR>Rack R<VAR>G : Type u_2<VAR>Group G<VAR>f : R →◃ Quandle.Conj G<VAR>g : Rack.EnvelGroup R →* G<VAR>h : f = (Quandle.Conj.map g).comp (Rack.toEnvelGroup R)<GOAL>g = Rack.toEnvelGroup.map f
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(Rack.envelAction ((Rack.toEnvelGroup R) x)) y = x ◃ y
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>self : DirectSum.GAlgebra R A<VAR>r : R<VAR>x : GradedMonoid A<GOAL>r • x = GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r) * x
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>self : DirectSum.GAlgebra R A<GOAL>DirectSum.GAlgebra.toFun 1 = GradedMonoid.GOne.one
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>self : DirectSum.GAlgebra R A<VAR>r s : R<GOAL>GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun (r * s)) = GradedMonoid.mk (0 + 0) (GradedMonoid.GMul.mul (DirectSum.GAlgebra.toFun r) (DirectSum.GAlgebra.toFun s))
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>self : DirectSum.GAlgebra R A<VAR>r : R<VAR>x : GradedMonoid A<GOAL>GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r) * x = x * GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r)
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>DirectSum.GAlgebra R A<VAR>r : R<GOAL>(algebraMap R (DirectSum ι fun i => A i)) r = (DirectSum.of A 0) (DirectSum.GAlgebra.toFun r)
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>DirectSum.GAlgebra R A<GOAL>↑(algebraMap R (DirectSum ι fun i => A i)) = (DirectSum.of A 0).comp DirectSum.GAlgebra.toFun
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>B : Type uB<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring B<VAR>DirectSum.GAlgebra R A<VAR>Algebra R B<VAR>f : (i : ι) → A i →ₗ[R] B<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>a : DirectSum ι fun i => A i<GOAL>(DirectSum.toAlgebra R A f hone hmul) a = (DirectSum.toSemiring (fun i => (f i).toAddMonoidHom) hone hmul) a
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>B : Type uB<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring B<VAR>DirectSum.GAlgebra R A<VAR>Algebra R B<VAR>f g : (DirectSum ι fun i => A i) →ₐ[R] B<VAR>h : ∀ (i : ι), f.toLinearMap ∘ₗ DirectSum.lof R ι A i = g.toLinearMap ∘ₗ DirectSum.lof R ι A i<GOAL>f = g
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>B : Type uB<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring B<VAR>DirectSum.GAlgebra R A<VAR>Algebra R B<VAR>f g : (DirectSum ι fun i => A i) →ₐ[R] B<VAR>h : ∀ (i : ι) (x : A i), f ((DirectSum.of A i) x) = g ((DirectSum.of A i) x)<GOAL>f = g
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (A i)<VAR>(i : ι) → Module R (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>DirectSum.GAlgebra R A<VAR>i j : ι<VAR>a : A i<VAR>b : A j<GOAL>((DirectSum.gMulLHom R A) a) b = GradedMonoid.GMul.mul a b
<VAR>ι : Type uι<VAR>R : Type u_1<VAR>A : Type u_2<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>∀ (a : R), DirectSum.GAlgebra.toFun a = (↑↑(algebraMap R A)).toFun a
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommGroup (β i)<VAR>g₁ g₂ : DirectSum ι fun i => β i<VAR>i : ι<GOAL>(g₁ - g₂) i = g₁ i - g₂ i
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>i : ι<GOAL>0 i = 0
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>g₁ g₂ : DirectSum ι fun i => β i<VAR>i : ι<GOAL>(g₁ + g₂) i = g₁ i + g₂ i
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>i : ι<VAR>x : β i<GOAL>((DirectSum.of β i) x) i = x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>x : β i<VAR>h : i ≠ j<GOAL>((DirectSum.of β i) x) j = 0
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>i : ι<VAR>j : ι<VAR>x : β i<GOAL>((DirectSum.of β i) x) j = if h : i = j then Eq.recOn h x else 0
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>f : (i : ↑↑s) → β ↑i<VAR>n : ι<VAR>hn : n ∈ s<GOAL>((DirectSum.mk β s) f) n = f ⟨n, hn⟩
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>f : (i : ↑↑s) → β ↑i<VAR>n : ι<VAR>hn : n ∉ s<GOAL>((DirectSum.mk β s) f) n = 0
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<GOAL>DFinsupp.support 0 = ∅
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>x : β i<VAR>h : x ≠ 0<GOAL>DFinsupp.support ((DirectSum.of β i) x) = {i}
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>b : β i<GOAL>DFinsupp.support ((DirectSum.of β i) b) ⊆ {i}
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>x : DirectSum ι fun i => β i<GOAL>∑ i ∈ DFinsupp.support x, (DirectSum.of β i) (x i) = x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>Fintype ι<VAR>x : DirectSum ι fun i => β i<GOAL>∑ i : ι, (DirectSum.of β i) (x i) = x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>s : Finset ι<GOAL>Function.Injective ⇑(DirectSum.mk β s)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>Function.Injective ⇑(DirectSum.of β i)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>C : (DirectSum ι fun i => β i) → Prop<VAR>x : DirectSum ι fun i => β i<VAR>H_zero : C 0<VAR>H_basic : ∀ (i : ι) (x : β i), C ((DirectSum.of β i) x)<VAR>H_plus : ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)<GOAL>C x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u_1<VAR>AddMonoid γ<VAR>f g : (DirectSum ι fun i => β i) →+ γ<VAR>H : ∀ (i : ι) (y : β i), f ((DirectSum.of β i) y) = g ((DirectSum.of β i) y)<GOAL>f = g
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u_1<VAR>AddMonoid γ<VAR>f g : (DirectSum ι fun i => β i) →+ γ<VAR>H : ∀ (i : ι), f.comp (DirectSum.of β i) = g.comp (DirectSum.of β i)<GOAL>f = g
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u₁<VAR>AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>i : ι<VAR>x : β i<GOAL>(DirectSum.toAddMonoid φ) ((DirectSum.of β i) x) = (φ i) x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u₁<VAR>AddCommMonoid γ<VAR>ψ : (DirectSum ι fun i => β i) →+ γ<VAR>f : DirectSum ι fun i => β i<GOAL>ψ f = (DirectSum.toAddMonoid fun i => ψ.comp (DirectSum.of β i)) f
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u₁<VAR>AddCommMonoid γ<GOAL>Function.Injective DirectSum.toAddMonoid
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u₁<VAR>AddCommMonoid γ<VAR>f g : (i : ι) → β i →+ γ<GOAL>DirectSum.toAddMonoid f = DirectSum.toAddMonoid g ↔ f = g
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u₁<VAR>AddCommMonoid γ<VAR>i : ι<VAR>f : γ →+ β i<GOAL>DirectSum.fromAddMonoid ((DirectSum.of (fun i => γ →+ β i) i) f) = (DirectSum.of β i).comp f
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>DecidableEq ι<VAR>γ : Type u₁<VAR>AddCommMonoid γ<VAR>i : ι<VAR>f : γ →+ β i<VAR>x : γ<GOAL>(DirectSum.fromAddMonoid ((DirectSum.of (fun i => γ →+ β i) i) f)) x = (DirectSum.of β i) (f x)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>(i : ι) → AddCommMonoid (β i)<VAR>κ : Type u_1<VAR>h : ι ≃ κ<VAR>f : DirectSum ι fun i => β i<VAR>k : κ<GOAL>((DirectSum.equivCongrLeft h) f) k = f (h.symm k)
<VAR>ι : Type v<VAR>α : Option ι → Type w<VAR>(i : Option ι) → AddCommMonoid (α i)<VAR>f : (fun i => α i) none × Π₀ (i : ι), (fun i => α i) (some i)<GOAL>(DirectSum.addEquivProdDirectSum.symm f).support' = Trunc.map (fun s => ⟨none ::ₘ Multiset.map some ↑s, ⋯⟩) f.2.support'
<VAR>ι : Type v<VAR>α : Option ι → Type w<VAR>(i : Option ι) → AddCommMonoid (α i)<VAR>f : (fun i => α i) none × Π₀ (i : ι), (fun i => α i) (some i)<VAR>i : Option ι<GOAL>(DirectSum.addEquivProdDirectSum.symm f) i = match i with | none => f.1 | some val => f.2 val
<VAR>ι : Type v<VAR>α : Option ι → Type w<VAR>(i : Option ι) → AddCommMonoid (α i)<VAR>f : Π₀ (i : Option ι), (fun i => α i) i<GOAL>DirectSum.addEquivProdDirectSum f = (f none, DFinsupp.comapDomain some ⋯ f)
<VAR>ι : Type v<VAR>DecidableEq ι<VAR>α : ι → Type u<VAR>δ : (i : ι) → α i → Type w<VAR>(i : ι) → (j : α i) → AddCommMonoid (δ i j)<VAR>f : DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd<VAR>i : ι<VAR>j : α i<GOAL>((DirectSum.sigmaCurry f) i) j = f ⟨i, j⟩
<VAR>ι : Type v<VAR>DecidableEq ι<VAR>α : ι → Type u<VAR>δ : (i : ι) → α i → Type w<VAR>(i : ι) → (j : α i) → AddCommMonoid (δ i j)<VAR>f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j<VAR>i : ι<VAR>j : α i<GOAL>(DirectSum.sigmaUncurry f) ⟨i, j⟩ = (f i) j
<VAR>ι : Type v<VAR>DecidableEq ι<VAR>M : Type u_1<VAR>S : Type u_2<VAR>DecidableEq M<VAR>AddCommMonoid M<VAR>SetLike S M<VAR>AddSubmonoidClass S M<VAR>A : ι → S<VAR>x : DirectSum ι fun i => ↥(A i)<GOAL>(DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun i x => ↑x
<VAR>ι : Type v<VAR>M : Type u_1<VAR>S : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike S M<VAR>AddSubmonoidClass S M<VAR>A : ι → S<VAR>i : ι<VAR>x : ↥(A i)<GOAL>(DirectSum.coeAddMonoidHom A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
<VAR>ι : Type v<VAR>M : Type u_1<VAR>S : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike S M<VAR>AddSubmonoidClass S M<VAR>A : ι → S<VAR>i j : ι<VAR>x : ↥(A i)<GOAL>↑(((DirectSum.of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)
<VAR>ι : Type v<VAR>M : Type u_1<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>A : ι → AddSubmonoid M<VAR>h : DirectSum.IsInternal A<GOAL>iSup A = ⊤
<VAR>ι : Type v<VAR>M : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid M<VAR>SetLike S M<VAR>AddSubmonoidClass S M<VAR>DecidableEq ι<VAR>DecidableEq M<VAR>A : ι → S<VAR>x : DirectSum ι fun i => ↥(A i)<GOAL>(Function.support fun i => ↑(x i)) ⊆ ↑(DFinsupp.support x)
<VAR>ι : Type v<VAR>M : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid M<VAR>SetLike S M<VAR>AddSubmonoidClass S M<VAR>A : ι → S<VAR>x : DirectSum ι fun i => ↥(A i)<GOAL>(Function.support fun i => ↑(x i)).Finite
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<VAR>K.HasHomology j<GOAL>K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<VAR>K.HasHomology j<GOAL>K.pOpcycles i ≫ K.opcyclesToCycles i j ≫ K.iCycles j = K.d i j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<VAR>K.HasHomology j<GOAL>K.pOpcycles i ≫ K.opcyclesToCycles i j = K.toCycles i j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<VAR>K.HasHomology j<GOAL>K.homologyι i ≫ K.opcyclesToCycles i j = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<VAR>K.HasHomology j<GOAL>K.opcyclesToCycles i j ≫ K.homologyπ j = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i j : ι<VAR>K.HasHomology i<VAR>K.HasHomology j<VAR>L.HasHomology i<VAR>L.HasHomology j<GOAL>HomologicalComplex.opcyclesMap φ i ≫ L.opcyclesToCycles i j = K.opcyclesToCycles i j ≫ HomologicalComplex.cyclesMap φ j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<GOAL>(HomologicalComplex.natTransOpCyclesToCycles C c i j).app K = K.opcyclesToCycles i j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>CategoryTheory.CategoryWithHomology C<GOAL>(HomologicalComplex.HomologySequence.composableArrows₃ K i j).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<GOAL>(HomologicalComplex.HomologySequence.composableArrows₃Functor C i j).map φ = CategoryTheory.ComposableArrows.homMk₃ (HomologicalComplex.homologyMap φ i) (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.cyclesMap φ j) (HomologicalComplex.homologyMap φ j) ⋯ ⋯ ⋯
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<GOAL>(HomologicalComplex.HomologySequence.composableArrows₃Functor C i j).obj K = HomologicalComplex.HomologySequence.composableArrows₃ K i j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>CategoryTheory.Epi S.g<VAR>i : ι<VAR>S.X₁.HasHomology i<VAR>S.X₂.HasHomology i<VAR>S.X₃.HasHomology i<GOAL>(CategoryTheory.ShortComplex.mk (HomologicalComplex.opcyclesMap S.f i) (HomologicalComplex.opcyclesMap S.g i) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>CategoryTheory.Mono S.f<VAR>i : ι<VAR>S.X₁.HasHomology i<VAR>S.X₂.HasHomology i<VAR>S.X₃.HasHomology i<GOAL>(CategoryTheory.ShortComplex.mk (HomologicalComplex.cyclesMap S.f i) (HomologicalComplex.cyclesMap S.g i) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₀₁ = S.mapNatTrans (HomologicalComplex.natTransHomologyι C c i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₂₃ = S.mapNatTrans (HomologicalComplex.natTransHomologyπ C c j)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₁ = (HomologicalComplex.opcyclesFunctor C c i).mapShortComplex.obj S
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₀ = (HomologicalComplex.homologyFunctor C c i).mapShortComplex.obj S
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₂ = (HomologicalComplex.cyclesFunctor C c j).mapShortComplex.obj S
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₃ = (HomologicalComplex.homologyFunctor C c j).mapShortComplex.obj S
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₁₂ = S.mapNatTrans (HomologicalComplex.natTransOpCyclesToCycles C c i j)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>hS.δ i j hij ≫ HomologicalComplex.homologyMap S.f j = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>HomologicalComplex.homologyMap S.g i ≫ hS.δ i j hij = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(CategoryTheory.ShortComplex.mk (hS.δ i j hij) (HomologicalComplex.homologyMap S.f j) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i : ι<GOAL>(CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.g i) (hS.δ i j hij) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>x₃ : A ⟶ S.X₃.homology i<VAR>x₂ : A ⟶ S.X₂.opcycles i<VAR>x₁ : A ⟶ S.X₁.cycles j<VAR>h₂ : x₂ ≫ HomologicalComplex.opcyclesMap S.g i = x₃ ≫ S.X₃.homologyι i<VAR>h₁ : x₁ ≫ HomologicalComplex.cyclesMap S.f j = x₂ ≫ S.X₂.opcyclesToCycles i j<GOAL>x₃ ≫ hS.δ i j hij = x₁ ≫ S.X₁.homologyπ j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>x₃ : A ⟶ S.X₃.X i<VAR>hx₃ : x₃ ≫ S.X₃.d i j = 0<VAR>x₂ : A ⟶ S.X₂.X i<VAR>hx₂ : x₂ ≫ S.g.f i = x₃<VAR>x₁ : A ⟶ S.X₁.X j<VAR>hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j<VAR>k : ι<VAR>hk : c.next j = k<GOAL>S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij = S.X₁.liftCycles x₁ k hk ⋯ ≫ S.X₁.homologyπ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Coe α β<VAR>a b : α<GOAL>↑{ a := a, b := b } = { a := Coe.coe a, b := Coe.coe b }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Coe α β<VAR>g : GenContFract α<GOAL>↑g = { h := Coe.coe g.h, s := Stream'.Seq.map GenContFract.Pair.coeFn g.s }
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>GenContFract.IntFractPair.stream v 0 = some (GenContFract.IntFractPair.of v)
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_n : GenContFract.IntFractPair K<VAR>stream_nth_eq : GenContFract.IntFractPair.stream v n = some ifp_n<VAR>nth_fr_eq_zero : ifp_n.fr = 0<GOAL>GenContFract.IntFractPair.stream v (n + 1) = none
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>GenContFract.IntFractPair.stream v (n + 1) = none ↔ GenContFract.IntFractPair.stream v n = none ∨ ∃ ifp, GenContFract.IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_succ_n : GenContFract.IntFractPair K<GOAL>GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n ↔ ∃ ifp_n, GenContFract.IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ GenContFract.IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>p : GenContFract.IntFractPair K<VAR>h : GenContFract.IntFractPair.stream v n = some p<VAR>h' : p.fr ≠ 0<GOAL>GenContFract.IntFractPair.stream v (n + 1) = some (GenContFract.IntFractPair.of p.fr⁻¹)
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>a : ℤ<VAR>n : ℕ<GOAL>GenContFract.IntFractPair.stream (↑a) (n + 1) = none
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_succ_n : GenContFract.IntFractPair K<VAR>stream_succ_nth_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>succ_nth_fr_eq_zero : ifp_succ_n.fr = 0<GOAL>∃ ifp_n, GenContFract.IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋