ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β✝ : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<VAR>hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πS<VAR>πTβ : Set (Set ((i : { x // x ∈ T }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπT_pi : IsPiSystem πT<VAR>hπT_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πT<VAR>s : Set ((i : { x // x ∈ S }) → β ↑i)<VAR>sets_s : (i : { x // x ∈ S }) → Set (β ↑i)<VAR>hs1 : sets_s ∈ Set.univ.pi fun i => {s | MeasurableSet s}<VAR>hs2 : Set.univ.pi sets_s = s<VAR>t : Set ((i : { x // x ∈ T }) → β ↑i)<VAR>sets_t : (i : { x // x ∈ T }) → Set (β ↑i)<VAR>ht1 : sets_t ∈ Set.univ.pi fun i => {s | MeasurableSet s}<VAR>ht2 : Set.univ.pi sets_t = t<GOAL>∀ᵐ (a : α) ∂μ, (κ a) ((fun a i => f (↑i) a) ⁻¹' s ∩ (fun a i => f (↑i) a) ⁻¹' t) = (κ a) ((fun a i => f (↑i) a) ⁻¹' s) * (κ a) ((fun a i => f (↑i) a) ⁻¹' t)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β✝ : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<VAR>hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πS<VAR>πTβ : Set (Set ((i : { x // x ∈ T }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπT_pi : IsPiSystem πT<VAR>hπT_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πT<VAR>s : Set ((i : { x // x ∈ S }) → β ↑i)<VAR>sets_s : (i : { x // x ∈ S }) → Set (β ↑i)<VAR>hs2 : Set.univ.pi sets_s = s<VAR>t : Set ((i : { x // x ∈ T }) → β ↑i)<VAR>sets_t : (i : { x // x ∈ T }) → Set (β ↑i)<VAR>ht2 : Set.univ.pi sets_t = t<VAR>hs1 : ∀ (i : { x // x ∈ S }), MeasurableSet (sets_s i)<VAR>ht1 : ∀ (i : { x // x ∈ T }), MeasurableSet (sets_t i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) ((fun a i => f (↑i) a) ⁻¹' s ∩ (fun a i => f (↑i) a) ⁻¹' t) = (κ a) ((fun a i => f (↑i) a) ⁻¹' s) * (κ a) ((fun a i => f (↑i) a) ⁻¹' t)
<VAR>x y : ℝ*<GOAL>x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos
<VAR>x y : ℝ*<GOAL>(-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>h : some a ∈ (flatten (Applicative.toFunctor.1 (fun o => Option.recOn o nil Prod.snd) s.destruct)).destruct<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct >>= destruct<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>h : some a ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct >>= destruct<VAR>t : WSeq α<VAR>tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct<VAR>td : some a ∈ t.destruct<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>t : WSeq α<VAR>tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct<VAR>td : some a ∈ t.destruct<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>t : WSeq α<VAR>tm : t ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct<VAR>td : some a ∈ t.destruct<VAR>t' : Option (α × WSeq α)<VAR>ht' : t' ∈ s.destruct<VAR>ht2 : Option.rec nil Prod.snd t' = t<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>t : WSeq α<VAR>td : some a ∈ t.destruct<VAR>t' : Option (α × WSeq α)<VAR>ht' : t' ∈ s.destruct<VAR>ht2 : Option.rec nil Prod.snd t' = t<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>t : WSeq α<VAR>ht' : none ∈ s.destruct<VAR>ht2 : Option.rec nil Prod.snd none = t<VAR>td : some a ∈ Computation.pure none<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α × WSeq α<VAR>t : WSeq α<VAR>t' : α × WSeq α<VAR>td : some a ∈ t'.2.destruct<VAR>ht' : some t' ∈ s.destruct<VAR>ht2 : Option.rec nil Prod.snd (some t') = t<GOAL>∃ a', some a' ∈ s.destruct
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>(⋃ n, (x ^ n).support).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>∀ x_1 ∈ x.support, 0 ≤ x_1
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>⋃ n, (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<VAR>n : ℕ<GOAL>(x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : IndepFun X Y μ<VAR>h_int_X : Integrable (fun ω => rexp (t * X ω)) μ<VAR>h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ<VAR>hμ : ¬μ = 0<GOAL>cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : IndepFun X Y μ<VAR>h_int_X : Integrable (fun ω => rexp (t * X ω)) μ<VAR>h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ<VAR>hμ : ¬μ = 0<GOAL>log (mgf X μ t * mgf Y μ t) = log (mgf X μ t) + log (mgf Y μ t)
<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 : M →ₗ[R] M₂<VAR>x : M × M₂<GOAL>x ∈ range (inr R M M₂) ↔ x ∈ ker (fst R M M₂)
<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 : M →ₗ[R] M₂<VAR>x : M × M₂<GOAL>(∃ y, (inr R M M₂) y = x) ↔ (fst R M M₂) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m' : Multiset α<VAR>h : m ≤ m'<GOAL>m.sym2 ≤ m'.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m' : Multiset α<VAR>h✝ : m ≤ m'<VAR>xs ys : List α<VAR>h : ⟦xs⟧ ≤ ⟦ys⟧<GOAL>Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m' : Multiset α<VAR>h✝ : m ≤ m'<VAR>xs ys : List α<VAR>h : ⟦xs⟧ ≤ ⟦ys⟧<GOAL>xs <+~ ys
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.homologicalKernel.W f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<GOAL>F.homologicalKernel.W f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<GOAL>F.homologicalKernel.P (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<VAR>h₁ : ∀ (n : ℤ), IsZero (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).X₂ ↔ (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).f = 0 ∧ (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).g = 0<GOAL>F.homologicalKernel.P (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<VAR>h₁ : ∀ (n : ℤ), IsZero (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).X₂ ↔ (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).f = 0 ∧ (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).g = 0<VAR>h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map (Triangle.mk f g h).mor₁) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0<GOAL>F.homologicalKernel.P (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<VAR>h₁ : ∀ (n : ℤ), IsZero (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).X₂ ↔ (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).f = 0 ∧ (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).g = 0<VAR>h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map (Triangle.mk f g h).mor₁) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0<VAR>h₃ : ∀ (n : ℤ), Epi ((F.shift n).map (Triangle.mk f g h).mor₁) ↔ (F.shift n).map (Triangle.mk f g h).mor₂ = 0<GOAL>F.homologicalKernel.P (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<VAR>h₁ : ∀ (n : ℤ), IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0<VAR>h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0<VAR>h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0<GOAL>F.homologicalKernel.P Z ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_4, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.108053, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_5, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<VAR>h₁ : ∀ (n : ℤ), IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0<VAR>h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0<VAR>h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0<GOAL>(∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>α β : Type u<VAR>inst✝ : LawfulMonad m<VAR>f : β → α → m β<VAR>x✝ y✝ : FreeMonoid α<GOAL>{ toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun (x✝ * y✝) = { toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun x✝ * { toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun y✝
<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>α β : Type u<VAR>inst✝ : LawfulMonad m<VAR>f : β → α → m β<VAR>x✝ y✝ : FreeMonoid α<GOAL>unop ({ toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun (x✝ * y✝)) = unop ({ toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun x✝ * { toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun y✝)
<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>α β : Type u<VAR>inst✝ : LawfulMonad m<VAR>f : β → α → m β<VAR>x✝¹ y✝ : FreeMonoid α<VAR>x✝ : KleisliCat.mk m β<GOAL>unop ({ toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun (x✝¹ * y✝)) x✝ = unop ({ toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun x✝¹ * { toFun := fun xs => op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun y✝) x✝
<VAR>ι✝ : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ✝ : ι✝ → Type u_5<VAR>s s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α✝<VAR>f✝ g : ι✝ → α✝<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : CommSemiring α<VAR>f : ι → α<VAR>n : ℕ<GOAL>(∑ a : ι, f a) ^ n = ∑ p : Fin n → ι, ∏ i : Fin n, f (p i)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>x₀ : X<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>P : X → Y → Prop<VAR>hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in 𝓝 (x₀, y), P z.1 z.2<GOAL>∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>x₀ : X<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>P : X → Y → Prop<VAR>hP : ∀ᶠ (z : X × Y) in 𝓝 x₀ ×ˢ 𝓝ˢ K, P z.1 z.2<GOAL>∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁵ : Semifield K<VAR>inst✝⁴ : Semifield K₂<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module K V<VAR>inst✝¹ : AddCommMonoid V₂<VAR>inst✝ : Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>a : K<GOAL>range (a • f) = ⨆ (_ : a ≠ 0), range f
<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>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>s1 : AffineSubspace k P<VAR>h : s ⊆ ↑s1<VAR>p p1 : P<VAR>hp1 : p1 ∈ s<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>hp : p = v +ᵥ p1<GOAL>v +ᵥ p1 ∈ ↑s1
<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>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>s1 : AffineSubspace k P<VAR>h : s ⊆ ↑s1<VAR>p p1 : P<VAR>hp1 : p1 ∈ s<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>hp : p = v +ᵥ p1<VAR>hp1s1 : p1 ∈ ↑s1<GOAL>v +ᵥ p1 ∈ ↑s1
<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>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>s1 : AffineSubspace k P<VAR>h : s ⊆ ↑s1<VAR>p p1 : P<VAR>hp1 : p1 ∈ s<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>hp : p = v +ᵥ p1<VAR>hp1s1 : p1 ∈ ↑s1<GOAL>v ∈ s1.direction
<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>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>s1 : AffineSubspace k P<VAR>h : s ⊆ ↑s1<VAR>p p1 : P<VAR>hp1 : p1 ∈ s<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>hp : p = v +ᵥ p1<VAR>hp1s1 : p1 ∈ ↑s1<VAR>hs : vectorSpan k s ≤ s1.direction<GOAL>v ∈ s1.direction
<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>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>s1 : AffineSubspace k P<VAR>h : s ⊆ ↑s1<VAR>p p1 : P<VAR>hp1 : p1 ∈ s<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>hp : p = v +ᵥ p1<VAR>hp1s1 : p1 ∈ ↑s1<VAR>hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s1.direction<GOAL>v ∈ s1.direction
<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>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>s1 : AffineSubspace k P<VAR>h : s ⊆ ↑s1<VAR>p p1 : P<VAR>hp1 : p1 ∈ s<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>hp : p = v +ᵥ p1<VAR>hp1s1 : p1 ∈ ↑s1<VAR>hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s1.direction<GOAL>v ∈ ↑s1.direction
<VAR>g✝ : SL(2, ℤ)<VAR>z✝ : ℍ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>-g • z = g • z
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I✝<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>I : Box ι<GOAL>(l.toFilter I).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π}